Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/dependabot.yml
Original file line number Diff line number Diff line change
Expand Up @@ -4,4 +4,4 @@ updates:
- package-ecosystem: github-actions
directory: /
schedule:
interval: weekly
interval: monthly
19 changes: 10 additions & 9 deletions .github/workflows/main.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,15 +16,14 @@ jobs:
strategy:
fail-fast: false
matrix:
dune-version: [3.19.1]
dune-version: [3.20.2]
ocaml-version: [5.3.0]
camlp5-version: [8.03.06]
hol-light-version: [3.1.0]
hol-light-commit: [master]
hol-light-version: [3.0.0]
hol-light-commit: [72b2b70]
lambdapi-version: [master] # >= 3.0.0
rocq-version: [9.0.0]
dedukti-version: [2.7]
mapping: [mappings_N]
#rocq-version: [9.0.0]
runs-on: ubuntu-latest
steps:
# actions/checkout must be done BEFORE avsm/setup-ocaml
Expand All @@ -41,24 +40,26 @@ jobs:
eval `opam env`
dune build
dune install
- name: Install dependencies
- name: Install dedukti
run: |
opam install -y --deps-only hol_light.${{ matrix.hol-light-version }}
opam install -y dedukti.${{ matrix.dedukti-version }} rocq-prover.${{ matrix.rocq-version }}
opam install -y dedukti.${{ matrix.dedukti-version }}
- name: Install lambdapi
run: |
git clone --depth 1 -b ${{ matrix.lambdapi-version }} https://github.com/Deducteam/lambdapi
sudo apt-get install -y libev-dev
opam pin lambdapi lambdapi
opam install -y lambdapi
- name: Install HOL-Light dependencies
run: |
opam install -y --deps-only hol_light.${{ matrix.hol-light-version }}
- name: Get hol-light and patch it
run: |
eval `opam env`
export HOL2DK_DIR=`pwd`
export HOLLIGHT_DIR=`pwd`/hol-light
git clone https://github.com/jrh13/hol-light
cd hol-light
#git checkout ${{ matrix.hol-light-commit }}
git checkout ${{ matrix.hol-light-commit }}
make
hol2dk patch
- name: Dump proofs
Expand Down
2 changes: 1 addition & 1 deletion main.ml
Original file line number Diff line number Diff line change
Expand Up @@ -305,7 +305,7 @@ let print_hstats() =
let call_script s args =
match Sys.getenv_opt "HOL2DK_DIR" with
| None -> err "set $HOL2DK_DIR first\n"; exit 1
| Some d -> exit (Sys.command (d^"/"^s^" "^String.concat " " args))
| Some d -> exit (Sys.command ("sh "^d^"/"^s^" "^String.concat " " args))
;;

let print_env_var n =
Expand Down