X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2FREADME;h=1e7b2af63a49605db38b175da1d407d253b5ed71;hb=c450fdfb1b02eb69e5e7ef25f0acdf80157710df;hp=88067dee8bb2783f1e7934ea946e4bb8ed441d24;hpb=b37863d4598516a06241f18ad0db963399015bf2;p=helm.git

diff --git a/helm/software/helena/README b/helm/software/helena/README
index 88067dee8..1e7b2af63 100644
--- a/helm/software/helena/README
+++ b/helm/software/helena/README
@@ -2,20 +2,49 @@ 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 -0 (if unset, -0 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 all features enabled
+
+* Type "make byte" to compile the bytecode executable
+  with all features enabled
+
+* Type "make" or "make all" to compile both executables
+  with all features enabled
+
+* Type "make clean" to remove the products of compilation
+
+* Type "make ./helena.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 ./helena.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
+* Set at least F="" for targets:
+  test-si-fast test1 test2-opt test2-byte profile-fast profile profile-opt profile-byte
 
-* type "make profile" to validate the "grundlagen" 31 times
-  it generates etc/profile.txt with sorted execution times
+* Set at least F="TRACE" for targets:
+  test3 test6
+
+* Set at least F="SUMMARY PREPROCESS" for targets:
+  test-si
+
+* Set at least F="OBJECTS QUOTE" for targets:
+  xml-si xml-si-v3 xml xml-v3
+  
+* Set at least F="MANAGER QUOTE" for targets:
+  export-coq export-matita export-lp1 export-lp2 export-tj2 export-tj3 export-pts export-lyp
 
-* type "make profile-coq" to run coqc on the "grundlagen" 31 times
+* Type "make profile.opt" or "make profile.byte"
+  to validate the "grundlagen" 31 times (two runs each time)
   it generates etc/profile.txt with sorted execution times
-  coqc must be installed on your system