Merge pull request #429 from jfehrle/ltac2_debugger

Add a pick for 8.19.2 with the Ltac2 debugger (preview)
coq · Nov 19, 2024 · 1a7db05 · 1a7db05
2 parents b2b4f44 + 0b0c6e1
commit 1a7db05
Show file tree

Hide file tree

Showing 7 changed files with 535 additions and 0 deletions.
diff --git a/...core/coq-core.8.19.2.ltac2debug/files/0001-Windows-fix-path-normalization-in-coqdep.patch b/...core/coq-core.8.19.2.ltac2debug/files/0001-Windows-fix-path-normalization-in-coqdep.patch
@@ -0,0 +1,28 @@
+From 2b93006118401884a50d62013ce02cb1b7663c22 Mon Sep 17 00:00:00 2001
+From: Michael Soegtrop <[email protected]>
+Date: Thu, 3 Oct 2024 10:21:47 +0200
+Subject: [PATCH] Windows: fix path normalization in coqdep
+
+---
+ tools/coqdep/lib/file_util.ml | 5 +++--
+ 1 file changed, 3 insertions(+), 2 deletions(-)
+
+diff --git a/tools/coqdep/lib/file_util.ml b/tools/coqdep/lib/file_util.ml
+index 17d8622d78..77e9553810 100644
+--- a/tools/coqdep/lib/file_util.ml
++++ b/tools/coqdep/lib/file_util.ml
+@@ -10,8 +10,9 @@
+
+ let to_relative_path : string -> string = fun full_path ->
+   if Filename.is_relative full_path then full_path else
+-  let cwd  = String.split_on_char '/' (Sys.getcwd ()) in
+-  let path = String.split_on_char '/' full_path in
++  let re_delim = if Sys.win32 then "[/\\]" else "/" in
++  let cwd = Str.split_delim (Str.regexp re_delim) (Sys.getcwd ()) in
++  let path = Str.split_delim (Str.regexp re_delim) full_path in
+   let rec remove_common_prefix l1 l2 =
+     match (l1, l2) with
+     | (x1 :: l1, x2 :: l2) when x1 = x2 -> remove_common_prefix l1 l2
+-- 
+2.45.1
+
diff --git a/opam/opam-repository/packages/coq-core/coq-core.8.19.2.ltac2debug/opam b/opam/opam-repository/packages/coq-core/coq-core.8.19.2.ltac2debug/opam
@@ -0,0 +1,78 @@
+opam-version: "2.0"
+synopsis: "The Coq Proof Assistant -- Core Binaries and Tools"
+description: """
+Coq is a formal proof management system. It provides
+a formal language to write mathematical definitions, executable
+algorithms and theorems together with an environment for
+semi-interactive development of machine-checked proofs.
+
+Typical applications include the certification of properties of
+programming languages (e.g. the CompCert compiler certification
+project, or the Bedrock verified low-level programming library), the
+formalization of mathematics (e.g. the full formalization of the
+Feit-Thompson theorem or homotopy type theory) and teaching.
+
+This package includes the Coq core binaries, plugins, and tools, but
+not the vernacular standard library.
+
+Note that in this setup, Coq needs to be started with the -boot and
+-noinit options, as will otherwise fail to find the regular Coq
+prelude, now living in the coq-stdlib package."""
+maintainer: ["The Coq development team <[email protected]>"]
+authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+license: "LGPL-2.1-only"
+homepage: "https://coq.inria.fr/"
+doc: "https://coq.github.io/doc/"
+bug-reports: "https://github.com/coq/coq/issues"
+depends: [
+  "dune" {>= "2.9"}
+  "ocaml" {>= "4.09.0"}
+  "ocamlfind" {>= "1.8.1"}
+  "zarith" {>= "1.11"}
+  "conf-linux-libc-dev" {os = "linux"}
+  "odoc" {with-doc}
+]
+conflicts: [
+  "coq"   { < "8.17" }
+]
+depopts: ["coq-native" "memprof-limits"]
+dev-repo: "git+https://github.com/coq/coq.git"
+patches: [ 
+  "0001-Windows-fix-path-normalization-in-coqdep.patch"
+]
+build: [
+  ["dune" "subst"] {dev}
+  [ "./configure"
+    "-prefix" prefix
+    "-mandir" man
+    "-libdir" "%{lib}%/coq"
+    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
+  ]
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+
+url {
+  src: "https://github.com/jfehrle/coq/archive/refs/tags/debug_pl_8_19_tag2.tar.gz"
+  checksum: [
+    "md5=8540549341f6425174165edec2bc5c29"
+    "sha512=00833a93914d485e6ca695b6cec220da47957d7e3358bfe8e68300c48935255e95436be751826d837dfbd5f784116df86c1b57a8fe7e3301b45b4b19bffe958f"
+  ]
+}
+extra-files: [
+  [
+    "0001-Windows-fix-path-normalization-in-coqdep.patch"
+    "sha512=ed520c9e7d17f5bd9067e22d19983571cd88fbae7ae4c62cbc0daac9b607a357224b6e093c962858dd586ccd282d127bac565ed942d7025836e37b6635cbb609"
+  ]
+]
diff --git a/opam/opam-repository/packages/coq-stdlib/coq-stdlib.8.19.2.ltac2debug/opam b/opam/opam-repository/packages/coq-stdlib/coq-stdlib.8.19.2.ltac2debug/opam
@@ -0,0 +1,56 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "The Coq Proof Assistant -- Standard Library"
+description: """
+Coq is a formal proof management system. It provides
+a formal language to write mathematical definitions, executable
+algorithms and theorems together with an environment for
+semi-interactive development of machine-checked proofs.
+
+Typical applications include the certification of properties of
+programming languages (e.g. the CompCert compiler certification
+project, or the Bedrock verified low-level programming library), the
+formalization of mathematics (e.g. the full formalization of the
+Feit-Thompson theorem or homotopy type theory) and teaching.
+
+This package includes the Coq Standard Library, that is to say, the
+set of modules usually bound to the Coq.* namespace."""
+maintainer: ["The Coq development team <[email protected]>"]
+authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+license: "LGPL-2.1-only"
+homepage: "https://coq.inria.fr/"
+doc: "https://coq.github.io/doc/"
+bug-reports: "https://github.com/coq/coq/issues"
+depends: [
+  "dune" {>= "3.6"}
+  "coq-core" {= version}
+  "odoc" {with-doc}
+]
+depopts: ["coq-native"]
+dev-repo: "git+https://github.com/coq/coq.git"
+build: [
+  ["dune" "subst"] {dev}
+  # We tell dunestrap to use coq-config from coq-core
+  [ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" "DUNESTRAPOPT=-p coq-stdlib"]
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+url {
+  src:
+    "https://github.com/jfehrle/coq/archive/refs/tags/debug_pl_8_19_tag2.tar.gz"
+  checksum: [
+    "md5=8540549341f6425174165edec2bc5c29"
+    "sha512=00833a93914d485e6ca695b6cec220da47957d7e3358bfe8e68300c48935255e95436be751826d837dfbd5f784116df86c1b57a8fe7e3301b45b4b19bffe958f"
+  ]
+}
diff --git a/opam/opam-repository/packages/coq/coq.8.19.2.ltac2debug/opam b/opam/opam-repository/packages/coq/coq.8.19.2.ltac2debug/opam
@@ -0,0 +1,59 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "The Coq Proof Assistant"
+description: """
+Coq is a formal proof management system. It provides
+a formal language to write mathematical definitions, executable
+algorithms and theorems together with an environment for
+semi-interactive development of machine-checked proofs.
+
+Typical applications include the certification of properties of
+programming languages (e.g. the CompCert compiler certification
+project, or the Bedrock verified low-level programming library), the
+formalization of mathematics (e.g. the full formalization of the
+Feit-Thompson theorem or homotopy type theory) and teaching."""
+maintainer: ["The Coq development team <[email protected]>"]
+authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+license: "LGPL-2.1-only"
+homepage: "https://coq.inria.fr/"
+doc: "https://coq.github.io/doc/"
+bug-reports: "https://github.com/coq/coq/issues"
+depends: [
+  "dune" {>= "3.6"}
+  "coq-core" {= version}
+  "coq-stdlib" {= version}
+  "coqide-server" {= version}
+  "ounit2" {with-test}
+  "odoc" {with-doc}
+]
+dev-repo: "git+https://github.com/coq/coq.git"
+build: [
+  ["dune" "subst"] {dev}
+  [ "./configure"
+    "-prefix" prefix
+    "-mandir" man
+    "-libdir" "%{lib}%/coq"
+    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
+  ] {with-test}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+url {
+  src: 
+    "https://github.com/jfehrle/coq/archive/refs/tags/debug_pl_8_19_tag2.tar.gz"
+  checksum: [
+    "md5=8540549341f6425174165edec2bc5c29"
+    "sha512=00833a93914d485e6ca695b6cec220da47957d7e3358bfe8e68300c48935255e95436be751826d837dfbd5f784116df86c1b57a8fe7e3301b45b4b19bffe958f"
+  ]
+}
diff --git a/opam/opam-repository/packages/coqide-server/coqide-server.8.19.2.ltac2debug/opam b/opam/opam-repository/packages/coqide-server/coqide-server.8.19.2.ltac2debug/opam
@@ -0,0 +1,47 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "dev"
+synopsis: "The Coq Proof Assistant, XML protocol server"
+description: """
+Coq is a formal proof management system. It provides
+a formal language to write mathematical definitions, executable
+algorithms and theorems together with an environment for
+semi-interactive development of machine-checked proofs.
+
+This package provides the `coqidetop` language server, an
+implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md)
+which allows clients, such as CoqIDE, to interact with Coq in a
+structured way."""
+maintainer: ["The Coq development team <[email protected]>"]
+authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+license: "LGPL-2.1-only"
+homepage: "https://coq.inria.fr/"
+doc: "https://coq.github.io/doc/"
+bug-reports: "https://github.com/coq/coq/issues"
+depends: [
+  "dune" {>= "3.6"}
+  "coq-core" {= version}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/coq/coq.git"
+url {
+  src: "https://github.com/jfehrle/coq/archive/refs/tags/debug_pl_8_19_tag2.tar.gz"
+  checksum: [
+    "md5=8540549341f6425174165edec2bc5c29"
+    "sha512=00833a93914d485e6ca695b6cec220da47957d7e3358bfe8e68300c48935255e95436be751826d837dfbd5f784116df86c1b57a8fe7e3301b45b4b19bffe958f"
+  ]
+}
diff --git a/opam/opam-repository/packages/coqide/coqide.8.19.2.ltac2debug/opam b/opam/opam-repository/packages/coqide/coqide.8.19.2.ltac2debug/opam
@@ -0,0 +1,51 @@
+opam-version: "2.0"
+synopsis: "The Coq Proof Assistant --- GTK3 IDE"
+description: """
+Coq is a formal proof management system. It provides
+a formal language to write mathematical definitions, executable
+algorithms and theorems together with an environment for
+semi-interactive development of machine-checked proofs.
+
+This package provides the CoqIDE, a graphical user interface for the
+development of interactive proofs."""
+maintainer: ["The Coq development team <[email protected]>"]
+authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+license: "LGPL-2.1-only"
+homepage: "https://coq.inria.fr/"
+doc: "https://coq.github.io/doc/"
+bug-reports: "https://github.com/coq/coq/issues"
+depends: [
+  "dune" {>= "2.9"}
+  "ocamlfind" {build}
+  "conf-findutils" {build}
+  "conf-adwaita-icon-theme"
+  "coqide-server" {= version}
+  "cairo2" {>= "0.6.4"}
+  "lablgtk3-sourceview3" {>= "3.1.5"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+dev-repo: "git+https://github.com/coq/coq.git"
+
+url {
+  src: "https://github.com/jfehrle/coq/archive/refs/tags/debug_pl_8_19_tag2.tar.gz"
+  checksum: [
+    "md5=8540549341f6425174165edec2bc5c29"
+    "sha512=00833a93914d485e6ca695b6cec220da47957d7e3358bfe8e68300c48935255e95436be751826d837dfbd5f784116df86c1b57a8fe7e3301b45b4b19bffe958f"
+  ]
+}