X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2FREADME;h=37f553a25541c302e6993356d2aa72713f4bd258;hb=25893b01cb815cbd9a3b9684952bfc0f42c0739d;hp=646b3352622b5494344b25b9f53b30922d1236a6;hpb=bcc6a96020485731da4c02cc38043817903bd7dc;p=helm.git diff --git a/helm/software/helena/README b/helm/software/helena/README index 646b33526..37f553a25 100644 --- a/helm/software/helena/README +++ b/helm/software/helena/README @@ -9,20 +9,42 @@ 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) OBJECTS enable options -O -o (if unset, -o is disabled) -PREPROCESS enable option -p (if unset, -p 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 opt" to compile the native executable - with the desired features listed in the variable F +* 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 byte" to compile the bytecode executable +* Type "make ./helena.opt" to compile the native executable with the desired features listed in the variable F -* type "make" or "make all" to compile both executables +* Type "make ./helena.byte" to compile the bytecode executable with the desired features listed in the variable F -* type "make clean" to remove the products of compilation +* Set at least F="" for targets: + test-si-fast test1 test2-opt test2-byte profile-fast profile profile-opt profile-byte + +* 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 -* type "make profile" to validate 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