added environment file setting for each tutor

diff --git a/helm/hbugs/tutors/INDEX.xml b/helm/hbugs/tutors/INDEX.xml
index 7936066b28c399411778805dca8f616c2e12c9b0..bd4baad454b6dce9029fc53c2db73fa3540dca2d 100644 (file)
--- a/helm/hbugs/tutors/INDEX.xml
+++ b/helm/hbugs/tutors/INDEX.xml
@@ -11,6 +11,7 @@
   @HINT_TYPE@         hint type (3rd argument of Hbugs_types.Register_tutor type
                       constructor, must have type Hbugs_types.hint_type)
   @DESCRIPTION@       human readable tutor description
+  @ENVIRONMENT_FILE@  file from which restore proof checking environment on boot
 
   "source" attribute  corresponding OCaml source file
 
@@ -31,6 +32,7 @@
     <hint>Hbugs_types.Use_ring_Luke</hint>
     <hint_type>Use Ring Luke</hint_type>
     <description>WAIT FOREVER tutor</description>
+    <environment_file>wait.environment</environment_file>
   </tutor>
 -->
 
@@ -41,6 +43,7 @@
     <hint>Hbugs_types.Use_ring_Luke</hint>
     <hint_type>Use Ring Luke</hint_type>
     <description>Ring tutor</description>
+    <environment_file>ring.environment</environment_file>
   </tutor>
   <tutor source="fourier_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -49,6 +52,7 @@
     <hint>Hbugs_types.Use_fourier_Luke</hint>
     <hint_type>Use Fourier Luke</hint_type>
     <description>Fourier tutor</description>
+    <environment_file>fourier.environment</environment_file>
   </tutor>
   <tutor source="reflexivity_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -57,6 +61,7 @@
     <hint>Hbugs_types.Use_reflexivity_Luke</hint>
     <hint_type>Use Reflexivity Luke</hint_type>
     <description>Reflexivity tutor</description>
+    <environment_file>reflexivity.environment</environment_file>
   </tutor>
   <tutor source="symmetry_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -65,6 +70,7 @@
     <hint>Hbugs_types.Use_symmetry_Luke</hint>
     <hint_type>Use Symmetry Luke</hint_type>
     <description>Symmetry tutor</description>
+    <environment_file>symmetry.environment</environment_file>
   </tutor>
   <tutor source="assumption_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -73,6 +79,7 @@
     <hint>Hbugs_types.Use_assumption_Luke</hint>
     <hint_type>Use Assumption Luke</hint_type>
     <description>Assumption tutor</description>
+    <environment_file>assumption.environment</environment_file>
   </tutor>
   <tutor source="contradiction_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -81,6 +88,7 @@
     <hint>Hbugs_types.Use_contradiction_Luke</hint>
     <hint_type>Use Contradiction Luke</hint_type>
     <description>Contradiction tutor</description>
+    <environment_file>contradiction.environment</environment_file>
   </tutor>
   <tutor source="exists_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -89,6 +97,7 @@
     <hint>Hbugs_types.Use_exists_Luke</hint>
     <hint_type>Use Exists Luke</hint_type>
     <description>Exists tutor</description>
+    <environment_file>exists.environment</environment_file>
   </tutor>
   <tutor source="split_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -97,6 +106,7 @@
     <hint>Hbugs_types.Use_split_Luke</hint>
     <hint_type>Use Split Luke</hint_type>
     <description>Split tutor</description>
+    <environment_file>split.environment</environment_file>
   </tutor>
   <tutor source="left_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -105,6 +115,7 @@
     <hint>Hbugs_types.Use_left_Luke</hint>
     <hint_type>Use Left Luke</hint_type>
     <description>Left tutor</description>
+    <environment_file>left.environment</environment_file>
   </tutor>
   <tutor source="right_tutor.ml">
     <addr>127.0.0.1</addr>
@@ -113,15 +124,17 @@
     <hint>Hbugs_types.Use_right_Luke</hint>
     <hint_type>Use Right Luke</hint_type>
     <description>Right tutor</description>
+    <environment_file>right.environment</environment_file>
   </tutor>
   <tutor source="search_pattern_apply_tutor.ml">
-    <no_auto />
+    <no_auto /> <!-- this imply that settings below are not significant -->
     <addr>127.0.0.1</addr>
     <port>50011</port>
     <tactic>PrimitiveTactics.apply_tac</tactic>
     <hint>Hbugs_types.Use_apply_Luke</hint>
     <hint_type>Use Apply Luke (with argument)</hint_type>
     <description>Search pattern apply tutor</description>
+    <environment_file>search_pattern_apply.environment</environment_file>
   </tutor>
 </tutors>