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 succeed in 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]> 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
