From bc8b54f66e9e40155ddffd52c221cf06a7f2b0fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sat, 25 Jan 2025 13:20:38 +0100 Subject: [PATCH 1/4] Inf: remove builtins --- U/Inf.lp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/U/Inf.lp b/U/Inf.lp index af89525..c194cab 100644 --- a/U/Inf.lp +++ b/U/Inf.lp @@ -1,15 +1,15 @@ require open Logic.U.Set Logic.U.Prop; -constant symbol zero : El ι; builtin "0" ≔ zero; +constant symbol zero : El ι; -constant symbol succ : El ι → El ι; builtin "+1" ≔ succ; +constant symbol succ : El ι → El ι; symbol pred : El ι → El ι; -rule pred 0 ↪ 0 +rule pred zero ↪ zero with pred (succ $x) ↪ $x; symbol positive : El ι → Prop; -rule positive 0 ↪ ⊥ +rule positive zero ↪ ⊥ with positive (succ _) ↪ ⊤; From b3a3b45944c64edab9e5d942c054cc1c52bbd572 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sat, 25 Jan 2025 13:25:18 +0100 Subject: [PATCH 2/4] wip --- .github/dependabot.yml | 7 +++++++ .github/workflows/main.yml | 6 +++--- 2 files changed, 10 insertions(+), 3 deletions(-) create mode 100644 .github/dependabot.yml diff --git a/.github/dependabot.yml b/.github/dependabot.yml new file mode 100644 index 0000000..bc9a4d5 --- /dev/null +++ b/.github/dependabot.yml @@ -0,0 +1,7 @@ +version: 2 + +updates: + - package-ecosystem: github-actions + directory: / + schedule: + interval: weekly diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index e3dcc6b..53654d1 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -12,11 +12,11 @@ jobs: runs-on: ubuntu-latest steps: - name: Check out library - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Install ocaml and opam - uses: ocaml/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v3 with: - ocaml-compiler: 4.14.0 + ocaml-compiler: 5.2.1 - name: Install required libraries run: sudo apt-get install -y libev-dev - name: Setup opam for testing the development version From 747094daadad0d00e112dc9f8960e892581ff556 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sat, 25 Jan 2025 13:38:16 +0100 Subject: [PATCH 3/4] wip --- .github/workflows/main.yml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 53654d1..34eb0ec 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -8,7 +8,7 @@ jobs: strategy: fail-fast: false matrix: - lambdapi-version: [lambdapi, lambdapi.2.5.0, lambdapi.2.4.1, lambdapi.2.4.0, lambdapi.2.3.1, lambdapi.2.3.0, lambdapi.2.2.1, lambdapi.2.2.0, lambdapi.2.1.0, lambdapi.2.0.0] + lambdapi-version: [lambdapi, lambdapi.2.5.1, lambdapi.2.5.0, lambdapi.2.4.1, lambdapi.2.4.0, lambdapi.2.3.1, lambdapi.2.3.0, lambdapi.2.2.1, lambdapi.2.2.0, lambdapi.2.1.0, lambdapi.2.0.0] runs-on: ubuntu-latest steps: - name: Check out library @@ -16,7 +16,8 @@ jobs: - name: Install ocaml and opam uses: ocaml/setup-ocaml@v3 with: - ocaml-compiler: 5.2.1 + ocaml-compiler: 4.14.2 + # lambdapi.2.3.0 dependencies require ocaml < 5.0.0 - name: Install required libraries run: sudo apt-get install -y libev-dev - name: Setup opam for testing the development version From 6608d039ded5f1a74891ac72e3be8fdc303838c2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sat, 25 Jan 2025 13:38:36 +0100 Subject: [PATCH 4/4] wip --- .github/workflows/main.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 34eb0ec..13bd921 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -1,6 +1,6 @@ on: pull_request: - types: [opened, synchronize, edited, reopened] + types: [opened, synchronize, reopened] push: workflow_dispatch: jobs: