From a83b4694d712795bbb5977fd18b41716d92ea2bc Mon Sep 17 00:00:00 2001 From: Alidra <40537601+Alidra@users.noreply.github.com> Date: Tue, 24 Sep 2024 10:38:46 +0200 Subject: [PATCH 1/5] Fix Vscode extension : Prevent Goals panel to take focus when browsing proofs (#1134) * vscode: remove debugin message * vscode: set preserveFocus to true to prevent Goals panel from taking focus each time --- editors/vscode/src/client.ts | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/editors/vscode/src/client.ts b/editors/vscode/src/client.ts index 362ba7463..ccf3951c3 100644 --- a/editors/vscode/src/client.ts +++ b/editors/vscode/src/client.ts @@ -704,9 +704,8 @@ function sendGoalsRequest(position: Position, panel: WebviewPanel, docUri: Uri, return; } // Take focus back if the goal panel lost it. - window.showErrorMessage("Going through Goals"); if(!panel.active) { - panel.reveal(2, false); + panel.reveal(2, true); } updateTerminalText(goals.logs); From 3d519c5818893e58997c9ffe47d0489985ef4b64 Mon Sep 17 00:00:00 2001 From: Alidra <40537601+Alidra@users.noreply.github.com> Date: Mon, 30 Sep 2024 12:13:17 +0200 Subject: [PATCH 2/5] Release minor version 0.2.2.1 (#1135) * vscode: remove debugin message * vscode: set preserveFocus to true to prevent Goals panel from taking focus each time * vscode: release minor revision to bring Goals panel to front whithout taking focus --- editors/vscode/package.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/editors/vscode/package.json b/editors/vscode/package.json index e173c9d3f..fb7e5e3e9 100644 --- a/editors/vscode/package.json +++ b/editors/vscode/package.json @@ -8,7 +8,7 @@ "François Lefoulon ", "Ashish Barnawal " ], - "version": "0.2.2", + "version": "0.2.3", "publisher": "Deducteam", "engines": { "vscode": "^1.82.0" From 7f6e007f5646be743113ad09b899135191546e28 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 10 Oct 2024 17:55:55 +0200 Subject: [PATCH 3/5] fix induction command (issue #1141) (#1142) --- src/handle/tactic.ml | 1 + tests/OK/1141.lp | 8 ++++++++ tests/OK/922.lp | 2 +- tests/OK/Prop.lp | 2 +- tests/export_raw_dk.sh | 2 +- 5 files changed, 12 insertions(+), 3 deletions(-) create mode 100644 tests/OK/1141.lp diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index e8f767aec..c14f55c5d 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -145,6 +145,7 @@ let ind_data : popt -> Env.t -> term -> Sign.ind_data = fun pos env a -> begin try let ind = SymMap.find s !(sign.sign_ind) in + let _, ts = List.cut ts ind.ind_nb_params (*remove parameters*) in let ctxt = Env.to_ctxt env in if LibTerm.distinct_vars ctxt (Array.of_list ts) = None then fatal pos "%a is not applied to distinct variables." sym s diff --git a/tests/OK/1141.lp b/tests/OK/1141.lp new file mode 100644 index 000000000..26272c6f5 --- /dev/null +++ b/tests/OK/1141.lp @@ -0,0 +1,8 @@ +require open tests.OK.Set tests.OK.Prop tests.OK.Nat tests.OK.List; + +symbol sample_1 (list : 𝕃 nat) : π ⊤ ≔ +begin + induction + { apply ⊤ᵢ } + { assume x l ih; apply ih } +end; diff --git a/tests/OK/922.lp b/tests/OK/922.lp index f048a0d4e..8ef5ccfee 100644 --- a/tests/OK/922.lp +++ b/tests/OK/922.lp @@ -20,5 +20,5 @@ with is0 (_ +1) ↪ false; opaque symbol s≠0 [n] : π (n +1 ≠ 0) ≔ begin - assume n h; refine ind_eq h (λ n, istrue(is0 n)) top + assume n h; refine ind_eq h (λ n, istrue(is0 n)) ⊤ᵢ end; diff --git a/tests/OK/Prop.lp b/tests/OK/Prop.lp index 0dda7b4f4..5c8e28ffa 100644 --- a/tests/OK/Prop.lp +++ b/tests/OK/Prop.lp @@ -14,7 +14,7 @@ builtin "P" ≔ π; constant symbol ⊤ : Prop; // \top -constant symbol top : π ⊤; +constant symbol ⊤ᵢ : π ⊤; // false diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh index d5fdd057f..3425632b2 100755 --- a/tests/export_raw_dk.sh +++ b/tests/export_raw_dk.sh @@ -60,7 +60,7 @@ do # proofs why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit);; # "open" - triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215);; + triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215|1141);; # "inductive" strictly_positive_*|inductive|989|904|830|341);; # underscore in query From 954d9a131971576f29f764d0922a9d1f0b775c88 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 30 Oct 2024 10:10:05 +0900 Subject: [PATCH 4/5] ci: test ocaml 4.14.2 instead of 4.14.1 (#1146) --- .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 cb9075934..d5d2e1a01 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -8,7 +8,7 @@ jobs: strategy: fail-fast: false matrix: - ocaml-version: [5.2.0, 5.1.1, 5.0.0, 4.14.1, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1] + ocaml-version: [5.2.0, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1] runs-on: ubuntu-latest steps: - name: checking out lambdapi repo ... From 3223066d349e37d4ac57a0b7e2f7a125fdf06044 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 30 Oct 2024 10:10:31 +0900 Subject: [PATCH 5/5] Doc: clarify ac canonical forms (#1147) --- doc/commands.rst | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/doc/commands.rst b/doc/commands.rst index 38b7d95a5..1d1e33c0f 100644 --- a/doc/commands.rst +++ b/doc/commands.rst @@ -128,14 +128,14 @@ the system with additional information on its properties and behavior. for every canonical term of the form ``f t u``, we have ``t ≤ u``, where ``≤`` is a total ordering on terms left unspecified. - If a symbol ``f`` is ``associative left`` then there is no - canonical term of the form ``f t (f u v)`` and thus every - canonical term headed by ``f`` is of the form ``f … (f (f t₁ t₂) - t₃) … tₙ``. If a symbol ``f`` is ``associative`` or ``associative - right`` then there is no canonical term of the form ``f (f t u) - v`` and thus every canonical term headed by ``f`` is of the form - ``f t₁ (f t₂ (f t₃ … tₙ) … )``. Moreover, in both cases, if ``f`` - is also ``commutative`` then we have ``t₁ ≤ t₂ ≤ … ≤ tₙ``. + If a symbol ``f`` is ``commutative`` and ``associative left`` then + there is no canonical term of the form ``f t (f u v)`` and thus + every canonical term headed by ``f`` is of the form ``f … (f (f t₁ + t₂) t₃) … tₙ``. If a symbol ``f`` is ``commutative`` and + ``associative`` or ``associative right`` then there is no + canonical term of the form ``f (f t u) v`` and thus every + canonical term headed by ``f`` is of the form ``f t₁ (f t₂ (f t₃ … + tₙ) … )``. Moreover, in both cases, we have ``t₁ ≤ t₂ ≤ … ≤ tₙ``. - **Exposition modifiers** define how a symbol can be used outside the module where it is defined. By default, the symbol can be used