Use ocaml setup, more opam

.github/workflows/check_encoding.yml

@@ -4,11 +4,7 @@ name: check_encoding
 
 # Controls when the action will run. Triggers the workflow on push or pull request
 # events but only for the master branch
-on:
-  push:
-    branches: [ master ]
-  pull_request:
-    branches: [ master ]
+on: [push]
 
 # A workflow run is made up of one or more jobs that can run sequentially or in parallel
 jobs:
@@ -23,34 +19,15 @@ jobs:
     - name: checking out personoj
       uses: actions/checkout@v2
 
-    - name: recovering cached opam files...
-      uses: actions/cache@v2
-      with:
-        path: ~/.opam
-        key: ${{ runner.os }}-ocaml-4.11.1
+    - name: Use opam
+      uses: ocaml/setup-ocaml@v2
 
-    - name: setting up opam
-      uses: avsm/setup-ocaml@v1
-      with:
-        ocaml-version: 4.11.1
-
-    - name: get lambdapi
-      uses: actions/checkout@v2
-      with:
-        repository: gabrielhdt/lambdapi
-        ref: refiner
-        path: lambdapi
-
-    # Runs a set of commands using the runners shell
-    - name: install lambdapi and deps
+    - name: Install lambdapi
       run: |
-        sudo apt install --yes bmake perl
-        (cd "${GITHUB_WORKSPACE}/lambdapi/" || exit 1
-         opam install .)
-        eval $(opam env)
-        why3 config detect
+        opam pin add 'git://github.com/gabrielhdt/lambdapi#refiner'
+        opam exec -- why3 config detect
 
     - name: check encoding
       run: |
-        eval $(opam env)
-        bmake encoding
+        yes | sudo apt install bmake
+        opam exec -- bmake encoding

.github/workflows/proof_tools.yml

@@ -4,6 +4,13 @@ on: [push]
 
 jobs:
   build:
+    strategy:
+      fail-fast: false
+      matrix:
+        ocaml-compiler:
+          - 4.08.x
+          - 4.13.x
+
     runs-on: ubuntu-latest
 
     steps:
@@ -11,20 +18,31 @@ jobs:
       with:
         path: personoj
 
-    - name: setup
-      run: ${GITHUB_WORKSPACE}/personoj/tools/bootstrap.sh
-      shell: sh
+    - name: Use ocaml
+      uses: ocaml/setup-ocaml@v2
+      with:
+        ocaml-compiler: ${{ matrix.ocaml-compiler }}
+
+    - name: Pin lambdapi
+      run: opam pin add 'git://github.com/gabrielhdt/lambdapi#refiner'
+
+    - name: dopth
+      run: |
+        cd "${GITHUB_WORKSPACE}"/personoj/proofs/dopth || exit 1
+        opam install dune --yes
+        opam exec -- dune build
+        opam exec -- dune runtest
+
+    - name: chainprops
+      run: |
+        cd "${GITHUB_WORKSPACE}"/personoj/proofs/chainprops || exit 1
+        opam install . --deps-only --yes
+        opam exec -- dune build
+        opam exec -- dune runtest
 
-    - name: compile and run tests
+    - name: appaxiom
       run: |
-        cd "${GITHUB_WORKSPACE}"/personoj/proofs/ || exit 1
-        (cd dopth || exit 1
-         opam switch create . --packages dune --yes
-         eval $(opam env)
-         bmake tests)
-        (cd chainprops || exit 1
-         opam switch create . --deps-only --yes
-         eval $(opam env)
-         opam pin add ~/lambdapi --yes
-         eval $(opam env)
-         bmake tests)
+        cd "${GITHUB_WORKSPACE}"/personoj/proofs/appaxiom || exit 1
+        opam install . --deps-only --yes
+        opam exec -- dune build
+        opam exec -- dune runtest

.github/workflows/pvs_prelude.yml

@@ -11,20 +11,26 @@ jobs:
       with:
         path: personoj
 
-    - name: setup
-      run: ${GITHUB_WORKSPACE}/personoj/tools/bootstrap.sh
+    - name: setup ocaml
+      uses: ocaml/setup-ocaml@v2
+      with:
+        ocaml-compiler: 4.11.1
+
+    - name: pin lambdapi
+      run: opam pin add 'git://github.com/gabrielhdt/lambdapi#refiner'
+
+    - name: Install PVS
+      run: ${GITHUB_WORKSPACE}/personoj/tools/setup-pvs.sh
       shell: sh
 
     - name: install personoj
       run: |
-        eval $(opam env --switch=~/lambdapi --set-switch)
-        bmake -C "${GITHUB_WORKSPACE}"/personoj/encoding install
+        opam exec -- bmake -C "${GITHUB_WORKSPACE}"/personoj/encoding install
         cp "${GITHUB_WORKSPACE}/personoj/tools/load-personoj.lisp" ~/.pvs.lisp
         echo '(load-personoj)' >> ~/.pvs.lisp
 
     - name: translate and typecheck
       run: |
-        eval $(opam env --switch=~/lambdapi --set-switch)
         cd "${GITHUB_WORKSPACE}"/personoj/specs/tools/prelude || exit 1
         # Comment out theories that consume too much memory during 
         # typechecking
@@ -32,4 +38,4 @@ jobs:
         sed -i 's/^modulo_arithmetic$/-modulo_arithmetic/' theories
         sed -i 's/^mod$/-mod/' theories
         PERSONOJPATH="${GITHUB_WORKSPACE}"/personoj/
-        bmake PERSONOJPATH="${PERSONOJPATH}" PVSPATH=~/PVS
+        opam exec -- bmake PERSONOJPATH="${PERSONOJPATH}" PVSPATH=~/PVS

proofs/appaxiom/appaxiom.opam

 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
+synopsis: "Apply something on Dedukti axioms"
+maintainer: ["dedukti-dev@inria.fr"]
 depends: [
   "dune" {>= "2.9"}
   "cmdliner"

proofs/appaxiom/dune-project

@@ -2,6 +2,9 @@
 (cram enable)
 (generate_opam_files true)
 
+(maintainers "dedukti-dev@inria.fr")
+
 (package
  (name appaxiom)
+ (synopsis "Apply something on Dedukti axioms")
  (depends cmdliner lambdapi))

proofs/chainprops/chainprops.opam

 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
+synopsis: "Make inference steps out of Dedukti propositions"
+maintainer: ["dedukti-dev@inria.fr"]
 depends: [
   "dune" {>= "2.9"}
   "cmdliner"

proofs/chainprops/dune-project

@@ -3,8 +3,10 @@
 (cram enable)
 
 (generate_opam_files true)
+(maintainers "dedukti-dev@inria.fr")
 
 (package
  (name chainprops)
+ (synopsis "Make inference steps out of Dedukti propositions")
  (depends
-  cmdliner angstrom))
+  cmdliner angstrom lambdapi))

tools/personoj.opam

+opam-version: "2.0"
+compiler: ["ocaml.4.11.1"]
+roots: [
+  "lambdapi.1.0"
+  "ocaml.4.11.1"
+  "ocaml-lsp-server.1.4.1"
+  "ocamlformat.0.19.0"
+  "ocamlformat-rpc.0.19.0"
+]
+installed: [
+  "astring.0.8.5"
+  "base.v0.14.1"
+  "base-bigarray.base"
+  "base-bytes.base"
+  "base-threads.base"
+  "base-unix.base"
+  "bindlib.5.0.1"
+  "biniou.1.2.1"
+  "cmdliner.1.0.4"
+  "cppo.1.6.8"
+  "csexp.1.5.1"
+  "dot-merlin-reader.4.1"
+  "dune.2.9.1"
+  "dune-build-info.2.9.1"
+  "dune-configurator.2.9.1"
+  "easy-format.1.3.2"
+  "fix.20201120"
+  "fpath.0.7.3"
+  "gen.0.5.3"
+  "lambdapi.1.0"
+  "menhir.20211012"
+  "menhirLib.20211012"
+  "menhirSdk.20211012"
+  "num.1.4"
+  "ocaml.4.11.1"
+  "ocaml-compiler-libs.v0.12.4"
+  "ocaml-config.1"
+  "ocaml-lsp-server.1.4.1"
+  "ocaml-system.4.11.1"
+  "ocamlbuild.0.14.0"
+  "ocamlfind.1.9.1"
+  "ocamlformat.0.19.0"
+  "ocamlformat-rpc.0.19.0"
+  "ocamlformat-rpc-lib.0.19.0"
+  "ocp-indent.1.8.1"
+  "odoc-parser.0.9.0"
+  "ppx_derivers.1.2.1"
+  "ppx_yojson_conv_lib.v0.14.0"
+  "ppxlib.0.23.0"
+  "pratter.1.2"
+  "re.1.10.3"
+  "result.1.5"
+  "sedlex.2.4"
+  "seq.base"
+  "sexplib0.v0.14.0"
+  "stdio.v0.14.0"
+  "stdlib-shims.0.3.0"
+  "timed.1.0"
+  "topkg.1.0.4"
+  "uchar.0.0.2"
+  "uucp.14.0.0"
+  "uuseg.14.0.0"
+  "uutf.1.0.2"
+  "why3.1.4.0"
+  "yojson.1.7.0"
+]
+pinned: "lambdapi.1.0"
+package "lambdapi" {
+  opam-version: "2.0"
+  version: "1.0"
+  synopsis: "Proof assistant based on the λΠ-calculus modulo rewriting"
+  description: """\
+Proof assistant based on the λΠ-calculus modulo rewriting,
+mostly compatible with Dedukti.
+
+This package contains both the `lambdapi` proof assistant and the `lp-lsp`
+Language Server Protocol helper for IDEs to check lambdapi files."""
+  maintainer: "dedukti-dev@inria.fr"
+  authors: "Deducteam"
+  license: "CECILL-2.1"
+  homepage: "https://github.com/Deducteam/lambdapi"
+  bug-reports: "https://github.com/Deducteam/lambdapi/issues"
+  depends: [
+    "dune" {>= "2.1"}
+    "ocaml" {>= "4.07.0"}
+    "menhir" {>= "20200624"}
+    "sedlex" {>= "2.2"}
+    "alcotest" {with-test}
+    "bindlib" {>= "5.0.1"}
+    "timed" {>= "1.0"}
+    "pratter" {>= "1.2"}
+    "why3" {>= "1.4.0"}
+    "yojson" {>= "1.6.0"}
+    "cmdliner" {>= "1.0.3"}
+    "stdlib-shims" {>= "0.1.0"}
+  ]
+  build: [
+    ["dune" "subst"] {pinned}
+    [
+      "dune"
+      "build"
+      "-p"
+      name
+      "-j"
+      jobs
+      "@install"
+      "@runtest" {with-test}
+      "@doc" {with-doc}
+    ]
+  ]
+  dev-repo: "git+https://github.com/Deducteam/lambdapi.git"
+  url {
+    src: "git://github.com/gabrielhdt/lambdapi#refiner"
+  }
+}

tools/bootstrap.sh → tools/setup-pvs.sh

@@ -5,16 +5,7 @@ SCRIPT=$(realpath "$0")
 DIR=$(dirname "$SCRIPT")
 ROOT=$(realpath "${DIR}/..") # Root of personoj repo
 
-## Opam
-
-yes | sudo apt-get -q install \
-	zlib1g-dev libx11-dev libgmp-dev bubblewrap m4 gcc autoconf \
-	make unzip pkg-config git rsync bmake gcc perl \
-	emacs-nox
-sudo sysctl kernel.unprivileged_userns_clone=1 
-yes '/usr/local/bin' | sudo bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --version 2.1.0"
-
-opam init --bare --no-setup -q
+sudo apt-get -q install bmake perl gcc git emacs-nox
 
 ## SBCL
 
@@ -23,26 +14,10 @@ url="https://downloads.sourceforge.net/project/sbcl/sbcl/1.4.16/sbcl-1.4.16-x86-
  curl "$url" -L | tar jx
  ln -s sbcl* sbcl)
 
-gclone () {
-    (cd "$HOME"
-     git clone "$1"
-     (cd "$2" || exit 1
-      git checkout "$3"))
-}
-
-# Lambdapi
-
-gclone https://github.com/gabrielhdt/lambdapi.git lambdapi 1a7031e4
-
-(cd "${HOME}/lambdapi" || exit 1
- opam switch create . --locked --deps-only --yes
- eval "$(opam env)"
- make install
- why3 config detect)
-
 # PVS
-
-gclone https://github.com/SRI-CSL/PVS.git PVS pvs7.1
+(cd "$HOME" || exit 1
+ git clone https://github.com/SRI-CSL/PVS.git -q
+ cd PVS && git checkout pvs7.1)
 
 (cd "${HOME}/PVS" || exit 1
  autoconf