diff --git a/.github/workflows/check_encoding.yml b/.github/workflows/check_encoding.yml
index 9621310b4c6a3746c775e07540ceed6e02d8cd0d..b6676a4afbfcc9602690bc6302cb13d0dedc47d4 100644
--- a/.github/workflows/check_encoding.yml
+++ b/.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
diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml
index f219314ab1d499769e5da85ed17cbf5a7834fef4..82d47017026ae989c0c576a592fd1f7a8badbb55 100644
--- a/.github/workflows/proof_tools.yml
+++ b/.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
diff --git a/.github/workflows/pvs_prelude.yml b/.github/workflows/pvs_prelude.yml
index bab941ebe75ea07b20dec55613f0a0338ed4eda5..d23b80a4150001521c012db144908b9bdb96d5d7 100644
--- a/.github/workflows/pvs_prelude.yml
+++ b/.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
diff --git a/proofs/appaxiom/appaxiom.opam b/proofs/appaxiom/appaxiom.opam
index 76392f44ef4b8182aa105a0743625d3a137b825c..b0418660e6cef4158b109a22dd9fb4d5ecf58c08 100644
--- a/proofs/appaxiom/appaxiom.opam
+++ b/proofs/appaxiom/appaxiom.opam
@@ -1,5 +1,7 @@
# 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"
diff --git a/proofs/appaxiom/dune-project b/proofs/appaxiom/dune-project
index c42bfe5bf97323c8f3946d145360b71f11b968c4..1c9b5d940764918fa8f3120ce39b2febde671f4f 100644
--- a/proofs/appaxiom/dune-project
+++ b/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))
diff --git a/proofs/chainprops/chainprops.opam b/proofs/chainprops/chainprops.opam
index c69df8e8146f2e8ab636088cf1ed40054718750f..79bc42c721470c50b69bc6a29e28d04a116572c5 100644
--- a/proofs/chainprops/chainprops.opam
+++ b/proofs/chainprops/chainprops.opam
@@ -1,5 +1,7 @@
# 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"
diff --git a/proofs/chainprops/dune-project b/proofs/chainprops/dune-project
index b2b9816a4da46ed318f63fa5d06f82eccb5922ca..fb65ab4c61d7c10fa59133a3f3ddf85e0e2ee837 100644
--- a/proofs/chainprops/dune-project
+++ b/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))
diff --git a/tools/bootstrap.sh b/tools/bootstrap.sh
deleted file mode 100755
index 52bd155ec10a876ba1ee96a6db30c32daa98445d..0000000000000000000000000000000000000000
--- a/tools/bootstrap.sh
+++ /dev/null
@@ -1,61 +0,0 @@
-#!/bin/sh
-set -eu
-
-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
-
-## SBCL
-
-url="https://downloads.sourceforge.net/project/sbcl/sbcl/1.4.16/sbcl-1.4.16-x86-64-linux-binary.tar.bz2"
-(cd "${HOME}" || exit 1
- 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}/PVS" || exit 1
- autoconf
- ./configure)
-
- EMACS="$(command -v emacs)"
- SBCLISP_HOME="${HOME}/sbcl"
- PVSPATH="${HOME}/PVS"
- export PVSPATH
-
- for p in $(find "${ROOT}"/specs/tools/prelude_patches -name '*.diff' | sort); do
- patch "${PVSPATH}/lib/prelude.pvs" "$p"
- done
-
- (cd "${PVSPATH}"
- make EMACS="$EMACS" SBCLISP_HOME="$SBCLISP_HOME" >output 2>&1)
diff --git a/tools/personoj.opam b/tools/personoj.opam
new file mode 100644
index 0000000000000000000000000000000000000000..a785608358c1a074a27cf06c2e174c03cf545b63
--- /dev/null
+++ b/tools/personoj.opam
@@ -0,0 +1,115 @@
+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"
+ }
+}
diff --git a/tools/setup-pvs.sh b/tools/setup-pvs.sh
new file mode 100755
index 0000000000000000000000000000000000000000..e6d49b611c8d1e0841215d789e0f6fc5c9c828e7
--- /dev/null
+++ b/tools/setup-pvs.sh
@@ -0,0 +1,36 @@
+#!/bin/sh
+set -eu
+
+SCRIPT=$(realpath "$0")
+DIR=$(dirname "$SCRIPT")
+ROOT=$(realpath "${DIR}/..") # Root of personoj repo
+
+sudo apt-get -q install bmake perl gcc git emacs-nox
+
+## SBCL
+
+url="https://downloads.sourceforge.net/project/sbcl/sbcl/1.4.16/sbcl-1.4.16-x86-64-linux-binary.tar.bz2"
+(cd "${HOME}" || exit 1
+ curl "$url" -L | tar jx
+ ln -s sbcl* sbcl)
+
+# PVS
+(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
+ ./configure)
+
+ EMACS="$(command -v emacs)"
+ SBCLISP_HOME="${HOME}/sbcl"
+ PVSPATH="${HOME}/PVS"
+ export PVSPATH
+
+ for p in $(find "${ROOT}"/specs/tools/prelude_patches -name '*.diff' | sort); do
+ patch "${PVSPATH}/lib/prelude.pvs" "$p"
+ done
+
+ (cd "${PVSPATH}"
+ make EMACS="$EMACS" SBCLISP_HOME="$SBCLISP_HOME" >output 2>&1)