helm/ocaml/hbugs/data/tutors_index.xml

   1 <!--
   2   Data used to fill template "hbugs_tutor.TPL.ml"
   3
   4   @ADDR@              tutor ip address
   5   @PORT@              tutor tcp port
   6   @TACTIC@            tactic to use (OCaml function, must have type
   7                       ProofEngineTypes.tactic)
   8   @HINT@              hint to be sent to client (content of Hbugs_types.Eureka
   9                       type constructor, must have type Hbugs_types.hint, see
  10                       hbugs_types.ml)
  11   @HINT_TYPE@         hint type (3rd argument of Hbugs_types.Register_tutor type
  12                       constructor, must have type Hbugs_types.hint_type)
  13   @DESCRIPTION@       human readable tutor description
  14   @ENVIRONMENT_FILE@  file from which restore proof checking environment on boot
  15
  16   "source" attribute  corresponding OCaml source file
  17
  18   INVARIANT:  XML element name below are lowercase version of @TAGS@ used in
  19               template
  20
  21   TODO: hint type isn't yet well formalized
  22 -->
  23
  24 <tutors>
  25
  26   <!-- DEBUGGING -->
  27 <!--
  28   <tutor source="wait_tutor.ml">
  29     <addr>127.0.0.1</addr>
  30     <port>50111</port>
  31     <tactic>Wait.wait_tac</tactic>
  32     <hint>Hbugs_types.Use_ring_Luke</hint>
  33     <hint_type>Use Ring Luke</hint_type>
  34     <description>WAIT FOREVER tutor</description>
  35     <environment_file>wait.environment</environment_file>
  36   </tutor>
  37 -->
  38
  39   <tutor source="ring_tutor.ml">
  40     <addr>127.0.0.1</addr>
  41     <port>50001</port>
  42     <tactic>Ring.ring_tac</tactic>
  43     <hint>Hbugs_types.Use_ring_Luke</hint>
  44     <hint_type>Use Ring Luke</hint_type>
  45     <description>Ring tutor</description>
  46     <environment_file>ring.environment</environment_file>
  47   </tutor>
  48   <tutor source="fourier_tutor.ml">
  49     <addr>127.0.0.1</addr>
  50     <port>50002</port>
  51     <tactic>FourierR.fourier_tac</tactic>
  52     <hint>Hbugs_types.Use_fourier_Luke</hint>
  53     <hint_type>Use Fourier Luke</hint_type>
  54     <description>Fourier tutor</description>
  55     <environment_file>fourier.environment</environment_file>
  56   </tutor>
  57   <tutor source="reflexivity_tutor.ml">
  58     <addr>127.0.0.1</addr>
  59     <port>50003</port>
  60     <tactic>EqualityTactics.reflexivity_tac</tactic>
  61     <hint>Hbugs_types.Use_reflexivity_Luke</hint>
  62     <hint_type>Use Reflexivity Luke</hint_type>
  63     <description>Reflexivity tutor</description>
  64     <environment_file>reflexivity.environment</environment_file>
  65   </tutor>
  66   <tutor source="symmetry_tutor.ml">
  67     <addr>127.0.0.1</addr>
  68     <port>50004</port>
  69     <tactic>EqualityTactics.symmetry_tac</tactic>
  70     <hint>Hbugs_types.Use_symmetry_Luke</hint>
  71     <hint_type>Use Symmetry Luke</hint_type>
  72     <description>Symmetry tutor</description>
  73     <environment_file>symmetry.environment</environment_file>
  74   </tutor>
  75   <tutor source="assumption_tutor.ml">
  76     <addr>127.0.0.1</addr>
  77     <port>50005</port>
  78     <tactic>VariousTactics.assumption_tac</tactic>
  79     <hint>Hbugs_types.Use_assumption_Luke</hint>
  80     <hint_type>Use Assumption Luke</hint_type>
  81     <description>Assumption tutor</description>
  82     <environment_file>assumption.environment</environment_file>
  83   </tutor>
  84   <tutor source="contradiction_tutor.ml">
  85     <addr>127.0.0.1</addr>
  86     <port>50006</port>
  87     <tactic>NegationTactics.contradiction_tac</tactic>
  88     <hint>Hbugs_types.Use_contradiction_Luke</hint>
  89     <hint_type>Use Contradiction Luke</hint_type>
  90     <description>Contradiction tutor</description>
  91     <environment_file>contradiction.environment</environment_file>
  92   </tutor>
  93   <tutor source="exists_tutor.ml">
  94     <addr>127.0.0.1</addr>
  95     <port>50007</port>
  96     <tactic>IntroductionTactics.exists_tac</tactic>
  97     <hint>Hbugs_types.Use_exists_Luke</hint>
  98     <hint_type>Use Exists Luke</hint_type>
  99     <description>Exists tutor</description>
 100     <environment_file>exists.environment</environment_file>
 101   </tutor>
 102   <tutor source="split_tutor.ml">
 103     <addr>127.0.0.1</addr>
 104     <port>50008</port>
 105     <tactic>IntroductionTactics.split_tac</tactic>
 106     <hint>Hbugs_types.Use_split_Luke</hint>
 107     <hint_type>Use Split Luke</hint_type>
 108     <description>Split tutor</description>
 109     <environment_file>split.environment</environment_file>
 110   </tutor>
 111   <tutor source="left_tutor.ml">
 112     <addr>127.0.0.1</addr>
 113     <port>50009</port>
 114     <tactic>IntroductionTactics.left_tac</tactic>
 115     <hint>Hbugs_types.Use_left_Luke</hint>
 116     <hint_type>Use Left Luke</hint_type>
 117     <description>Left tutor</description>
 118     <environment_file>left.environment</environment_file>
 119   </tutor>
 120   <tutor source="right_tutor.ml">
 121     <addr>127.0.0.1</addr>
 122     <port>50010</port>
 123     <tactic>IntroductionTactics.right_tac</tactic>
 124     <hint>Hbugs_types.Use_right_Luke</hint>
 125     <hint_type>Use Right Luke</hint_type>
 126     <description>Right tutor</description>
 127     <environment_file>right.environment</environment_file>
 128   </tutor>
 129   <tutor source="search_pattern_apply_tutor.ml">
 130     <no_auto /> <!-- this imply that settings below are not significant -->
 131     <addr>127.0.0.1</addr>
 132     <port>50011</port>
 133     <tactic>PrimitiveTactics.apply_tac</tactic>
 134     <hint>Hbugs_types.Use_apply_Luke</hint>
 135     <hint_type>Use Apply Luke (with argument)</hint_type>
 136     <description>Search pattern apply tutor</description>
 137     <environment_file>search_pattern_apply.environment</environment_file>
 138   </tutor>
 139 </tutors>
 140