From 7a82239dff7298f99b65fe5ed31fd0beb9f4834c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maja=20K=C4=85dzio=C5=82ka?= Date: Sat, 13 Jun 2026 15:28:55 +0200 Subject: [PATCH 1/3] Bump the recommended OCaml version to 4.14.2 The 4.14.2 patch release incorporates ocaml/ocaml#12577, which makes the toolchain compile without errors on new versions of GCC. This is already necessary to be able to set up the library on bleeding-edge systems, such as Arch Linux, and the requirement will spread as the GCC update trickles down across distributions. The CI is already set up to use the latest available OCaml release from the 4.14 branch. --- README.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 341cdfbb..75d19318 100644 --- a/README.md +++ b/README.md @@ -120,7 +120,7 @@ You can use `opam` to install the current state of this branch as follows. We recommend creating a fresh opam switch: ``` -opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda +opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.2+options,ocaml-option-flambda eval $(opam env) ``` @@ -129,15 +129,15 @@ Then the following commands install the library: ``` opam repo add coq-released https://coq.inria.fr/opam/released opam update -opam pin add coq-library-undecidability.dev+9.0 "https://github.com/uds-psl/coq-library-undecidability.git#rocq-9.0" +opam pin add coq-library-undecidability.dev+9.2 "https://github.com/uds-psl/coq-library-undecidability.git#rocq-9.2" ``` ### Manual installation -You need `Rocq 9.0` built on OCAML `>= 4.09.1` (but we recommend and test OCaml version `4.14.1+flambda`) and the Template-Coq part of the [MetaCoq](https://metacoq.github.io/) package for Coq. If you are using `opam 2` you can use the following commands to install the dependencies on a new switch: +You need `Rocq 9.2` built on OCAML `>= 4.09.1` (but we recommend and test OCaml version `4.14.2+flambda`) and the Template-Coq part of the [MetaCoq](https://metacoq.github.io/) package for Coq. If you are using `opam 2` you can use the following commands to install the dependencies on a new switch: ``` -opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda +opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.2+options,ocaml-option-flambda eval $(opam env) opam repo add rocq-released https://rocq-prover.org/opam/released opam update @@ -162,7 +162,7 @@ The library is compatible with Coq's compiled interfaces ([`vos`](https://coq.in #### Coq version -Be careful that this branch only compiles under `Coq 8.16`. If you want to use a different Coq version you have to change to a different branch. +Be careful that this branch only compiles under `Rocq 9.2`. If you want to use a different Coq version you have to change to a different branch. Due to compatibility issues, not every branch contains exactly the same problems. We recommend to use the newest branch if possible. From 2c91d87da0590120aa97b28699ab47906d51e880 Mon Sep 17 00:00:00 2001 From: DmxLarchey Date: Tue, 16 Jun 2026 11:40:14 +0200 Subject: [PATCH 2/3] removed a clear statement ... section variables now get erased when "destruct" as invoked on them --- theories/FOL/TRAKHTENBROT/enumerable.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/FOL/TRAKHTENBROT/enumerable.v b/theories/FOL/TRAKHTENBROT/enumerable.v index 4d6c70c0..4f5c8ad1 100644 --- a/theories/FOL/TRAKHTENBROT/enumerable.v +++ b/theories/FOL/TRAKHTENBROT/enumerable.v @@ -130,7 +130,7 @@ Section enumerable_definitions. Theorem type_enum_t_by_measure : type_enum_t. Proof using Hm. - apply constructive_choice in Hm; destruct Hm as (f & Hf); clear Hm. + apply constructive_choice in Hm; destruct Hm as (f & Hf). exists (fun j => let (a,n) := surj j in f a n). intros x. destruct (proj1 (Hf _ x) (Nat.le_refl _)) as (a & Ha). From ab57e07b9ac1aed2451874870ccf6041fc1b3a5d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maja=20K=C4=85dzio=C5=82ka?= Date: Tue, 16 Jun 2026 20:50:21 +0200 Subject: [PATCH 3/3] Fix compilation on Rocq-dev --- theories/HOU/firstorder.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/HOU/firstorder.v b/theories/HOU/firstorder.v index 15c1431c..8fc75980 100644 --- a/theories/HOU/firstorder.v +++ b/theories/HOU/firstorder.v @@ -920,7 +920,7 @@ Section FirstOrderDecidable. - Let free (k: nat) (x: nat) := x >= k. + Local Definition free (k: nat) (x: nat) := x >= k. Instance dec_free k: Dec1 (free k). Proof. unfold free; typeclasses eauto. Qed. @@ -1024,7 +1024,7 @@ Section FirstOrderDecidable. * specialize decr_typing with (L := rev L) as H9; simplify in H9; eauto. * eapply decr_unifies; eauto. specialize (unify_unifiable H' (AppR s T, AppR t T0)); cbn; auto. - * eapply lambda_free_normal. pose proof (free := fun (k: nat) (x: nat) => x >= k). + * eapply lambda_free_normal. eapply decr_lambda_free; intros; eapply LF. + intros (Delta & sigma & E1 & E2 & E3). asimpl in E2. eapply Lambda_injective in E2. @@ -1057,4 +1057,4 @@ Section FirstOrderDecidable. Qed. End FirstOrderDecidable. - \ No newline at end of file +