Thanks for the question Heiko.
I think Thomas’s answer is the best that can be done at the moment, but now
that I’m aware of the problem, I will adjust polyscripter to pay attention to
`INCLUDES =` lines in a Holmakefile, and perhaps also `-I` command-line options
passed to polyscripter.
With a little work, it might not even be necessary to manually `load` the
theories first: there’s no strong reason that I can see why the input lines
can’t be parsed for module references in the same way that the Emacs mode does.
(Indeed, if using Poly/ML this might even be possible in the interactive system
more generally.)
Michael
On 16/2/18, 18:05, "Heiko Becker" <hbec...@mpi-sws.org> wrote:
Hello everyone,
I am trying to use the polyscripter tool to generate some nice output
from my HOL4 definitions.
In my directory, I have a file aScript.sml with theorem b_def being
produced. After compiling with Holmake, I have the files aTheory.sml and
aTheory.sig, where aTheory.sig contains the theorem b_def as expected.
I am trying to produce a pretty-printed version of b_def in a file c.txt
that contains the following two lines:
>>__ open aTheory
##thm b_def
However, running $HOL_DIR/Manual/Tools/polyscripter < c.txt gives me an
error in the line with open aTheory, that aTheory has not been declared.
Putting
>> OS.FileSys.getDir()
will print the working directory I am in at the moment.
Can someone explain to me how to set up my files such that I can
reference other theories using polyscripter?
Thanks in advance,
Heiko
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
