]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/README
- conditional compilation continues ...
[helm.git] / helm / software / helena / README
index 88067dee8bb2783f1e7934ea946e4bb8ed441d24..646b3352622b5494344b25b9f53b30922d1236a6 100644 (file)
@@ -2,20 +2,27 @@ Helena 0.8.3 M
 
 <compile-time feature> ::=
 
+LEXER      enable option -L (if unset, -T 0 is implied)
+PARSER     enable option -P (if unset, -T 0 is implied)
+TRACE      enable full option -T (if unset, -T > 2 is disabled)
+SUMMARY    enable option -d (if unset, -d is disabled)
 EXPAND     enable option -g (if unset, -g is disabled)
 MANAGER    enable options -M -m -p (if unset, -m is disabled)
-PREPROCESS enable option (if unset, -0 is disabled)
+OBJECTS    enable options -O -o (if unset, -o is disabled)
+PREPROCESS enable option -p (if unset, -p is disabled)
+QUOTE      enable option -q (if unset, -q is disabled)
+TYPE       enable option -t (if unset, -t is disabled)
 
-* type "make" or "make opt" to compile the native executable
+* type "make opt" to compile the native executable
   with the desired features listed in the variable F
 
-* type "make clean" to remove the products of compilation
+* type "make byte" to compile the bytecode executable
+  with the desired features listed in the variable F
 
-- type "make export-coq" to build the "grundlagen" for Coq 8
+* type "make" or "make all" to compile both executables
+  with the desired features listed in the variable F
 
-* type "make profile" to validate the "grundlagen" 31 times
-  it generates etc/profile.txt with sorted execution times
+* type "make clean" to remove the products of compilation
 
-* type "make profile-coq" to run coqc on the "grundlagen" 31 times
+* type "make profile" to validate the "grundlagen" 31 times
   it generates etc/profile.txt with sorted execution times
-  coqc must be installed on your system