Merge pull request #141 from aqjune-aws/ver310

Increment the version, backport the update of opam file

Author: jrh13

.github/workflows/main.yml

@@ -25,7 +25,7 @@ jobs:
           sudo apt update && sudo apt install -y opam
           opam init --disable-sandboxing --compiler=4.06.0
           opam pin -y add camlp5 7.10
-          opam install -y num ledit
+          opam install -y num ledit camlp-streams ocamlfind
 
       - name: Checkout this repo
         uses: actions/checkout@v2
@@ -34,12 +34,12 @@ jobs:
 
       - name: Run
         run: |
-          set -e
+          set -xe
           cd hol-light
           eval $(opam env)
           make
           ./hol.sh 2>&1 | tee log.txt
-          ! grep "Error" log.txt
+          grep "Error" log.txt && exit 1
           grep "Camlp5 parsing version" log.txt
 
   test2:
@@ -59,26 +59,26 @@ jobs:
 
       - name: Run
         run: |
-          set -e
+          set -xe
           cd hol-light
           make switch
           eval $(opam env)
           make
           ./hol.sh 2>&1 | tee log.txt
-          ! grep "Error" log.txt
+          grep "Error" log.txt && exit 1
           grep "Camlp5 parsing version (HOL-Light)" log.txt
           cd ..
 
       - name: Run (HOLLIGHT_USE_MODULE=1)
         run: |
-          set -e
+          set -xe
           cd hol-light
           eval $(opam env)
           make clean
           export HOLLIGHT_USE_MODULE=1
           make
           ./hol.sh 2>&1 | tee log.txt
-          ! grep "Error" log.txt
+          grep "Error" log.txt && exit 1
           grep "Camlp5 parsing version (HOL-Light)" log.txt
           ./unit_tests.byte
           ./unit_tests.native
@@ -100,26 +100,26 @@ jobs:
 
       - name: Run
         run: |
-          set -e
+          set -xe
           cd hol-light
           make switch-5
           eval $(opam env)
           make
           ./hol.sh 2>&1 | tee log.txt
-          ! grep "Error" log.txt
+          grep "Error" log.txt && exit 1
           grep "Camlp5 parsing version (HOL-Light)" log.txt
           cd ..
 
       - name: Run (HOLLIGHT_USE_MODULE=1)
         run: |
-          set -e
+          set -xe
           cd hol-light
           eval $(opam env)
           make clean
           export HOLLIGHT_USE_MODULE=1
           make
           ./hol.sh 2>&1 | tee log.txt
-          ! grep "Error" log.txt
+          grep "Error" log.txt && exit 1
           grep "Camlp5 parsing version (HOL-Light)" log.txt
           ./unit_tests.byte
           ./unit_tests.native

hol.ml

@@ -9,7 +9,7 @@
 (*              (c) Copyright, John Harrison 1998-2007                       *)
 (* ========================================================================= *)
 
-let hol_version = "3.0.0+";;
+let hol_version = "3.1.0";;
 
 #directory "+compiler-libs";;
 

opam

@@ -1,6 +1,6 @@
 opam-version: "2.0"
 name: "hol_light"
-version: "3.0.0"
+version: "3.1.0"
 synopsis: "The HOL-Light interactive theorem prover"
 description: """
 HOL Light is a computer program written by John Harrison to help users prove
@@ -52,6 +52,7 @@ depends: [
    "ledit")
   |
   ("ocaml" {>= "4.14.0"} &
+   "ocaml-base-compiler" &
    "camlp5" {>= "8.0"} &
    "zarith" {>= "1.5"} &
    "ledit")