Helena 0.8.3 M ::= 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) 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 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 ./helena.byte" to compile the bytecode executable with the desired features listed in the variable F * 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 export-cc0 export-lyp * 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