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.
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
