Can you send me the file you're trying to build with Holmake? (Or a stripped down version, if you like.)
Thanks, Michael On 30/11/11 13:36, 康西楠 wrote: > 1)I had added "val _ = export_theory();" and I never see the > Exporting theory "theoryname" ... done. > message. > 2)No message appeared at last. I got the message “Created theory”, “Saved > definition” then got an unexpected end without message of 1), > 3)I can create a eucildTheory follow the example in kananaskis-7-tutorial, > and I got "euclidTheory.sml" as expected. > 4)I am a newcomer of our team, and we've never succeedin using Holmake to > package our proving for futhure sessions, so I am trying to solve it. > 5)Do you think a Q structure can cause someting wrong? > Arthur > > At 2011-11-29 12:03:47,"Michael Norrish" <[email protected] > <mailto:[email protected]>> wrote: >>1) Did you see a >> >> Exporting theory "theoryname" ... done. >> >>message? >> >>If not, your export_theory command is messed up. >> >>I'm guessing, but you do have to write >> >> val _ = export_theory() >> >>not >> >> val _ = export_theory >> >>2) Did you get an error message from Holmake about the script not generating >>the theory file correctly? >> >>The message would be something like >> >>Script file thyScript didn't produce thyTheory.sml; >> maybe need export_theory() at end of thyScript.sml >> >>3) If you run Holmake in the hol directory examples\MLsyntax does it work? >> >>4) What do you expect Holmake to do that it doesn't do? >> >>Best, >>Michael >> >>On 29/11/11 14:01, 康西楠 wrote: >>> Hi all. >>> >>> I’m currently having a problem about using the Holmake tool on >>> Windows XP. I tried to compile a script which all the theorems we had >>> proved interactively, and I added “open HolKernel boolLib Parse >>> bossLib” ,new_theory and export_theory to the script.When I running >>> it, I can see the HOL message “Created theory”, “Saved definition” >>> and “Saved theorem”, but files didn’t exported finally. >>> >>> I want to know what’s the point to use Holmake on Windows. >> >> > > > > > ------------------------------------------------------------------------------ > All the data continuously generated in your IT infrastructure > contains a definitive record of customers, application performance, > security threats, fraudulent activity, and more. Splunk takes this > data and makes sense of it. IT sense. And common sense. > http://p.sf.net/sfu/splunk-novd2d > > > > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ All the data continuously generated in your IT infrastructure contains a definitive record of customers, application performance, security threats, fraudulent activity, and more. Splunk takes this data and makes sense of it. IT sense. And common sense. http://p.sf.net/sfu/splunk-novd2d
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
