Skip to content

Latest commit

 

History

History
 
 

developers

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
To generate the list of files that poly uses when building HOL, try
something like

    ../bin/unquote < ../src/bool/boolScript.sml |
       ./genUseScript --hol /dev/stdin > usethis.ML

Follow up with

    poly --use usethis.ML

to get into a Poly/ML session with that early prefix of stuff built.

To handle something like pred_setScript and to do it one fell swoop, the following should work:

   (../bin/unquote < ../src/pred_set/src/pred_setScript.sml |
       ./genUseScript --hol /dev/stdin ;
    echo 'use "../src/pred_set/src/pred_setScript.sml";' ) | poly

and will deposit pred_setTheory.{sig,sml,dat} into your developers
directory.