make-all-poly, make-all-nj: restored to main directory as examples
authorlcp
Fri May 13 11:10:14 1994 +0200 (1994-05-13)
changeset 370e95e212512d1
parent 369 5a7194eeb4ed
child 371 3a853818f1d2
make-all-poly, make-all-nj: restored to main directory as examples
README: modified accordingly
README
make-all-nj
make-all-poly
src/Tools/make-all-nj
src/Tools/make-all-poly
     1.1 --- a/README	Wed May 11 12:29:34 1994 +0200
     1.2 +++ b/README	Fri May 13 11:10:14 1994 +0200
     1.3 @@ -20,8 +20,9 @@
     1.4  free and its code sometimes runs faster.  Both compilers are perfectly
     1.5  satisfactory for running Isabelle.
     1.6  
     1.7 -The Makefiles and make-all use enviroment variables that you should set
     1.8 -according to your site configuration.
     1.9 +The Makefiles and make-all use environment variables that you should set
    1.10 +according to your site configuration.  See file make-all-nj for an example
    1.11 +using the Bourne shell, sh.
    1.12  
    1.13  ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML
    1.14  images.  When using Poly/ML, ISABELLEBIN must be an absolute pathname (one
    1.15 @@ -48,6 +49,8 @@
    1.16  Other important files include...
    1.17    COPYRIGHT   		Copyright notice and Disclaimer of Warranty
    1.18    make-all		shell script for building entire system
    1.19 +  make-all-poly		sample make-all invocation for Poly/ML
    1.20 +  make-all-nj		sample make-all invocation for SML of NJ
    1.21    change_simp		shell script to help convert sources to new simplifier
    1.22    expandshort		shell script to expand "shortcuts" in files
    1.23    prove_goal.el       	Emacs command to change proof format
    1.24 @@ -65,11 +68,12 @@
    1.25    FOL 	  Natural deduction First-Order Logic (intuitionistic and classical)
    1.26    FOLP 	  First-Order Logic with Proof terms
    1.27    ZF	  Zermelo-Fraenkel set theory
    1.28 +  HOL	  Classical Higher-Order Logic
    1.29 +  LCF     Logic for Computable Functions (domain theory) built upon FOL
    1.30 +  HOLCF   A version of LCF built upon HOL
    1.31    CTT	  Constructive Type Theory
    1.32 -  HOL	  Classical Higher-Order Logic
    1.33    LK	  Classical first-order sequent calculus
    1.34    Modal	  The modal logics T, S4, S43
    1.35 -  LCF     Logic for Computable Functions (domain theory)
    1.36    CCL	  Martin Coen's Classical Computational Logic
    1.37    Cube	  Barendregt's Lambda Cube
    1.38  
    1.39 @@ -121,4 +125,4 @@
    1.40  D-80290 Muenchen
    1.41  Germany
    1.42  
    1.43 -Last updated 13 December 1993
    1.44 +Last updated 13 May 1994
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/make-all-nj	Fri May 13 11:10:14 1994 +0200
     2.3 @@ -0,0 +1,8 @@
     2.4 +#! /bin/sh
     2.5 +#Make entire system using Standard ML of New Jersey
     2.6 +#Pathnames will have to be modified for your site
     2.7 +ISABELLEBIN=/homes/`whoami`/bin
     2.8 +ISABELLECOMP=sml
     2.9 +ISABELLEMAKE=Makefile.NJ
    2.10 +export ISABELLEBIN ISABELLECOMP ISABELLEMAKE
    2.11 +nohup make-all $*
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/make-all-poly	Fri May 13 11:10:14 1994 +0200
     3.3 @@ -0,0 +1,9 @@
     3.4 +#! /bin/sh
     3.5 +#Make entire system using Poly/ML
     3.6 +#Pathnames will have to be modified for your site
     3.7 +ML_DBASE=/usr/groups/theory/poly/`arch`/ML_dbase
     3.8 +ISABELLEBIN=/homes/`whoami`/bin
     3.9 +ISABELLECOMP="poly -noDisplay -h 15000"
    3.10 +ISABELLEMAKE=Makefile
    3.11 +export ML_DBASE ISABELLEBIN ISABELLECOMP ISABELLEMAKE
    3.12 +nohup make-all $*
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/make-all-nj	Fri May 13 11:10:14 1994 +0200
     4.3 @@ -0,0 +1,8 @@
     4.4 +#! /bin/sh
     4.5 +#Make entire system using Standard ML of New Jersey
     4.6 +#Pathnames will have to be modified for your site
     4.7 +ISABELLEBIN=/homes/`whoami`/bin
     4.8 +ISABELLECOMP=sml
     4.9 +ISABELLEMAKE=Makefile.NJ
    4.10 +export ISABELLEBIN ISABELLECOMP ISABELLEMAKE
    4.11 +nohup make-all $*
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/make-all-poly	Fri May 13 11:10:14 1994 +0200
     5.3 @@ -0,0 +1,9 @@
     5.4 +#! /bin/sh
     5.5 +#Make entire system using Poly/ML
     5.6 +#Pathnames will have to be modified for your site
     5.7 +ML_DBASE=/usr/groups/theory/poly/`arch`/ML_dbase
     5.8 +ISABELLEBIN=/homes/`whoami`/bin
     5.9 +ISABELLECOMP="poly -noDisplay -h 15000"
    5.10 +ISABELLEMAKE=Makefile
    5.11 +export ML_DBASE ISABELLEBIN ISABELLECOMP ISABELLEMAKE
    5.12 +nohup make-all $*