Merge pull request #99 from aqjune/fixes

Pin camlp5 version of `make switch` to 8.02.01, fix typos in `NAME_ASSUMS_TAC` help
jrh13 · Jun 1, 2024 · ae6f821 · ae6f821
2 parents d836698 + cc63c85
commit ae6f821
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 8 deletions.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -42,15 +42,13 @@ jobs:
 
   test2:
     runs-on: ubuntu-22.04
-    name: OCaml 4.14, Camlp5 8.02
+    name: OCaml 4.14, Camlp5 8.02 (make switch)
 
     steps:
       - name: Install dependency
         run: |
           sudo apt update && sudo apt install -y opam xdot
-          opam init --disable-sandboxing --compiler=4.14.0
-          opam pin -y add camlp5 8.02.01
-          opam install -y zarith
+          opam init --disable-sandboxing
 
       - name: Checkout this repo
         uses: actions/checkout@v2
@@ -60,6 +58,7 @@ jobs:
       - name: Run
         run: |
           cd hol-light
+          make switch
           eval $(opam env)
           make
           ./hol.sh | tee log.txt

diff --git a/Help/NAME_ASSUMS_TAC.hlp b/Help/NAME_ASSUMS_TAC.hlp
@@ -1,6 +1,6 @@
-\DOC NAME_ASSUMS_LIST
+\DOC NAME_ASSUMS_TAC
 
-\TYPE {NAME_ASSUMS_LIST : tactic}
+\TYPE {NAME_ASSUMS_TAC : tactic}
 
 \SYNOPSIS
 Label unnamed assumptions.
@@ -9,7 +9,7 @@ Label unnamed assumptions.
 assumption.
 
 \DESCRIBE
-{NAME_ASSUMS_LIST} labels unnamed assumptions with "H0", "H1", ....
+{NAME_ASSUMS_TAC} labels unnamed assumptions with "H0", "H1", ....
 It skips named assumptions.
 
 \FAILURE

diff --git a/Makefile b/Makefile
@@ -44,7 +44,8 @@ default: update_database.ml pa_j.cmo hol.sh;
 switch:; \
   opam switch create . ocaml-base-compiler.4.14.0 ; \
   eval $(opam env) ; \
-  opam install -y zarith camlp5 ledit
+  opam install -y zarith ledit ; \
+  opam pin -y add camlp5 8.02.01
 
 # Choose an appropriate "update_database.ml" file