Hi Heiko, you need to load the theory before you can open it. Usually you don't need to take care of it yourself, because tools like Holmake or the emacs mode take care of it for you. However, for polyscripter you need a line like
>>__ load "aTheory" before you can open it. Often you want to load multiple theories, so "map load [...]" is useful. However, if you just add this line, it is quite likely that loading will fail, because the file "aTheory.ui" cannot be found. For files not in the current directory, you need to manually extend the loadpath via something like >>__ loadPath := newdir :: !loadPath; As an example let's say you want to use "latticeTheory" from "examples/separationLogic/src/". Then you need to build "latticeTheory.ui" (usually by running Holmake in that directory). Then you add >>__ loadPath := (Globals.HOLDIR ^ "/examples/separationLogic/src/") :: !loadPath; >>__ map load ["latticeTheory"] >>__ open latticeTheory >>- OPTION_SELECT_def Cheers Thomas P.S.: I was wondering, whether you have had a look at the munger. It is usually the one used to print existing definitions in Latex files. On 14.02.2018 13:17, Heiko Becker 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
