helm/software/helena/README

   1 Helena 0.8.3 M
   2
   3 <compile-time feature> ::=
   4
   5 LEXER      enable option -L (if unset, -T 0 is implied)
   6 PARSER     enable option -P (if unset, -T 0 is implied)
   7 TRACE      enable full option -T (if unset, -T > 2 is disabled)
   8 SUMMARY    enable option -d (if unset, -d is disabled)
   9 EXPAND     enable option -g (if unset, -g is disabled)
  10 MANAGER    enable options -M -m -p (if unset, -m is disabled)
  11 OBJECTS    enable options -O -o (if unset, -o is disabled)
  12 PREPROCESS enable option -0 (if unset, -0 is disabled)
  13 QUOTE      enable option -q (if unset, -q is disabled)
  14 TYPE       enable option -t (if unset, -t is disabled)
  15
  16 * Type "make opt" to compile the native executable
  17   with all features enabled
  18
  19 * Type "make byte" to compile the bytecode executable
  20   with all features enabled
  21
  22 * Type "make" or "make all" to compile both executables
  23   with all features enabled
  24
  25 * Type "make clean" to remove the products of compilation
  26
  27 * Type "make ./helena.opt" to compile the native executable
  28   with the desired features listed in the variable F
  29
  30 * Type "make ./helena.byte" to compile the bytecode executable
  31   with the desired features listed in the variable F
  32
  33 * Set at least F="" for targets:
  34   test-si-fast test1 test2-opt test2-byte profile-fast profile profile-opt profile-byte
  35
  36 * Set at least F="TRACE" for targets:
  37   test3 test6
  38
  39 * Set at least F="SUMMARY PREPROCESS" for targets:
  40   test-si
  41
  42 * Set at least F="OBJECTS QUOTE" for targets:
  43   xml-si xml-si-v3 xml xml-v3
  44
  45 * Set at least F="MANAGER QUOTE" for targets:
  46   export-coq export-matita export-lp1 export-lp2 export-tj2 export-tj3 export-cc0 export-lyp
  47
  48 * Type "make profile.opt" or "make profile.byte"
  49   to validate the "grundlagen" 31 times (two runs each time)
  50   it generates etc/profile.txt with sorted execution times