14 |
14 |
15 The Makefiles can use two different Standard ML compilers: Poly/ML version |
15 The Makefiles can use two different Standard ML compilers: Poly/ML version |
16 2.03 or later (from Abstract Hardware Ltd) and Standard ML of New Jersey |
16 2.03 or later (from Abstract Hardware Ltd) and Standard ML of New Jersey |
17 (Version 0.93 or later). Poly/ML is a commercial product and costs money, |
17 (Version 0.93 or later). Poly/ML is a commercial product and costs money, |
18 but it is reliable and its database system is convenient for interactive |
18 but it is reliable and its database system is convenient for interactive |
19 work. SML of New Jersey requires lots of memory and disc space, but it is |
19 work. SML of New Jersey requires lots of store and disc space, but it is |
20 free and its code sometimes runs faster. Both compilers are perfectly |
20 free and its code sometimes runs faster. Both compilers are perfectly |
21 satisfactory for running Isabelle. |
21 satisfactory for running Isabelle. |
22 |
22 |
23 The Makefiles and make-all use enviroment variables that you should set |
23 The Makefiles and make-all use enviroment variables that you should set |
24 according to your site configuration. |
24 according to your site configuration. |
25 |
25 |
26 ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML |
26 ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML |
27 images. When using Poly/ML, ISABELLEBIN must be an absolute pathname (one |
27 images. When using Poly/ML, ISABELLEBIN must be an absolute pathname (one |
28 starting with "/"). |
28 starting with "/"). |
29 |
29 |
30 ML_DBASE is an absolute pathname to the initial Poly/ML database (not |
30 ML_DBASE is an *absolute* pathname to the initial Poly/ML database (not |
31 required for New Jersey ML). |
31 required for New Jersey ML). |
32 |
32 |
33 ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "sml". If |
33 ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "sml". If |
34 ISABELLECOMP begins with the letters "poly" then the Makefiles assume that |
34 ISABELLECOMP begins with the letters "poly" then the Makefiles assume that |
35 it is Poly/ML; if it begins with the letters "sml" then they assume |
35 it is Poly/ML; if it begins with the letters "sml" then they assume |
77 These files can be loaded in batch mode. The commands can also be |
77 These files can be loaded in batch mode. The commands can also be |
78 executed interactively, using the windows on your workstation. This is a |
78 executed interactively, using the windows on your workstation. This is a |
79 good way to get started. |
79 good way to get started. |
80 |
80 |
81 Each object-logic is built on top of Pure Isabelle, and possibly on top of |
81 Each object-logic is built on top of Pure Isabelle, and possibly on top of |
82 another object logic (like FOL or LK). A database or binary called Pure is |
82 another object logic like FOL or LK. A database or binary called Pure is |
83 first created, then the object-logic is loaded on top. Poly/ML extends |
83 first created, then the object-logic is loaded on top. Poly/ML extends |
84 Pure using its "make_database" operation. Standard ML of New Jersey starts |
84 Pure using its "make_database" operation. Standard ML of New Jersey starts |
85 with the Pure core image and loads the object-logic's ROOT.ML. |
85 with the Pure core image and loads the object-logic's ROOT.ML. |
86 |
86 |
87 HOW TO GET A STANDARD ML COMPILER |
87 HOW TO GET A STANDARD ML COMPILER |
93 To obtain Standard ML of New Jersey, contact David MacQueen |
93 To obtain Standard ML of New Jersey, contact David MacQueen |
94 <dbm@com.att.research> at AT&T Bell Laboratories, 600 Mountain Avenue, |
94 <dbm@com.att.research> at AT&T Bell Laboratories, 600 Mountain Avenue, |
95 Murray Hill, NJ 07974, USA. This compiler is available by FTP. Connect to |
95 Murray Hill, NJ 07974, USA. This compiler is available by FTP. Connect to |
96 research.att.com; login as anonymous with your userid as password; set |
96 research.att.com; login as anonymous with your userid as password; set |
97 binary mode; transfer files from the directory dist/ml. |
97 binary mode; transfer files from the directory dist/ml. |
|
98 |
|
99 ------------------------------------------------------------------------------ |
|
100 |
|
101 The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum |
|
102 for Isabelle users to discuss problems and exchange information. To join, |
|
103 send a message to isabelle-users-request@cl.cam.ac.uk. |
98 |
104 |
99 ------------------------------------------------------------------------------ |
105 ------------------------------------------------------------------------------ |
100 |
106 |
101 Please report any problems you encounter. While we shall try to be helpful, |
107 Please report any problems you encounter. While we shall try to be helpful, |
102 we can accept no responsibility for the deficiences of Isabelle and their |
108 we can accept no responsibility for the deficiences of Isabelle and their |