diff --git a/.github/dependabot.yml b/.github/dependabot.yml index bc9a4d5..946aa41 100644 --- a/.github/dependabot.yml +++ b/.github/dependabot.yml @@ -4,4 +4,4 @@ updates: - package-ecosystem: github-actions directory: / schedule: - interval: weekly + interval: monthly diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 886c741..10e923d 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -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 @@ -41,16 +40,18 @@ 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` @@ -58,7 +59,7 @@ jobs: 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 diff --git a/main.ml b/main.ml index 0b07d3c..0e7f020 100644 --- a/main.ml +++ b/main.ml @@ -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 =