Tweaks

coq · Nov 16, 2024 · d37981a · d37981a
1 parent da2299f
commit d37981a
Show file tree

Hide file tree

Showing 7 changed files with 421 additions and 111 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/...tac2debug/files/PR19247-ported-Fix-coqide-compilation-with-lablgtk-3.1.5-on-windows.patch b/...tac2debug/files/PR19247-ported-Fix-coqide-compilation-with-lablgtk-3.1.5-on-windows.patch
@@ -0,0 +1,132 @@
+From 9642a39066364040d230feaba063ad266f8a59b3 Mon Sep 17 00:00:00 2001
+From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <[email protected]>
+Date: Wed, 19 Jun 2024 21:27:29 +0200
+Subject: [PATCH] Fix coqide compilation with lablgtk 3.1.5 on windows
+
+---
+ coqide.opam                   | 2 +-
+ dune-project                  | 2 +-
+ ide/coqide/coq.ml             | 5 +----
+ ide/coqide/coq.mli            | 3 ---
+ ide/coqide/coqide_WIN32.ml.in | 1 -
+ lib/spawn.ml                  | 7 ++-----
+ lib/spawn.mli                 | 3 +--
+ 7 files changed, 6 insertions(+), 17 deletions(-)
+
+diff --git a/coqide.opam b/coqide.opam
+index 6fd9e8d3ba..7a449542b2 100644
+--- a/coqide.opam
++++ b/coqide.opam
+@@ -23,7 +23,7 @@ depends: [
+   "conf-adwaita-icon-theme"
+   "coqide-server" {= version}
+   "cairo2" {>= "0.6.4"}
+-  "lablgtk3-sourceview3" {>= "3.1.2"}
++  "lablgtk3-sourceview3" {>= "3.1.5"}
+   "odoc" {with-doc}
+ ]
+ build: [
+diff --git a/dune-project b/dune-project
+index e730188086..060c3729b8 100644
+--- a/dune-project
++++ b/dune-project
+@@ -89,7 +89,7 @@ structured way."))
+   conf-adwaita-icon-theme
+   (coqide-server (= :version))
+   (cairo2 (>= 0.6.4))
+-  (lablgtk3-sourceview3 (>= 3.1.2)))
++  (lablgtk3-sourceview3 (>= 3.1.5)))
+  (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
+diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml
+index 6aec60c527..c5ac24489e 100644
+--- a/ide/coqide/coq.ml
++++ b/ide/coqide/coq.ml
+@@ -180,8 +180,6 @@ let breaker = ref (fun pid -> Unix.kill pid Sys.sigusr1)
+
+ (** * The structure describing a coqtop sub-process *)
+
+-let gio_channel_of_descr_socket = ref Glib.Io.channel_of_descr
+-
+ module GlibMainLoop = struct
+   type async_chan = Glib.Io.channel
+   type watch_id = Glib.Io.id
+@@ -190,8 +188,7 @@ module GlibMainLoop = struct
+     Glib.Io.add_watch ~cond:[`ERR; `HUP; `IN; `NVAL; `PRI] ~callback chan
+   let remove_watch x = try Glib.Io.remove x with Glib.GError _ -> ()
+   let read_all = Ideutils.io_read_all
+-  let async_chan_of_file fd = Glib.Io.channel_of_descr fd
+-  let async_chan_of_socket s = !gio_channel_of_descr_socket s
++  let async_chan_of_file_or_socket fd = Glib.Io.channel_of_descr fd
+ end
+
+ module CoqTop = Spawn.Async(GlibMainLoop)
+diff --git a/ide/coqide/coq.mli b/ide/coqide/coq.mli
+index 0b38c012aa..923a91f971 100644
+--- a/ide/coqide/coq.mli
++++ b/ide/coqide/coq.mli
+@@ -119,9 +119,6 @@ val get_arguments : coqtop -> string list
+ val set_arguments : coqtop -> string list -> unit
+ (** Set process arguments. This also forces a planned reset. *)
+
+-(** In win32, sockets are not like regular files *)
+-val gio_channel_of_descr_socket : (Unix.file_descr -> Glib.Io.channel) ref
+-
+ (** {5 Task processing} *)
+
+ val try_grab : ?db:bool -> coqtop -> unit task -> (unit -> unit) -> bool
+diff --git a/ide/coqide/coqide_WIN32.ml.in b/ide/coqide/coqide_WIN32.ml.in
+index b34204fdc6..2de6b5d059 100644
+--- a/ide/coqide/coqide_WIN32.ml.in
++++ b/ide/coqide/coqide_WIN32.ml.in
+@@ -48,7 +48,6 @@ let interrupter pid =
+   win32_interrupt pid
+
+ let () =
+-  Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket;
+   set_win32_path ();
+   Coq.interrupter := interrupter;
+   reroute_stdout_stderr ();
+diff --git a/lib/spawn.ml b/lib/spawn.ml
+index b509eb042b..ada7b36130 100644
+--- a/lib/spawn.ml
++++ b/lib/spawn.ml
+@@ -36,8 +36,7 @@ module type MainLoopModel = sig
+   val add_watch : callback:(condition list -> bool) -> async_chan -> watch_id
+   val remove_watch : watch_id -> unit
+   val read_all : async_chan -> string
+-  val async_chan_of_file : Unix.file_descr -> async_chan
+-  val async_chan_of_socket : Unix.file_descr -> async_chan
++  val async_chan_of_file_or_socket : Unix.file_descr -> async_chan
+ end
+
+ (* Common code *)
+@@ -191,9 +190,7 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ())
+   let pid, oob_resp, oob_req, cin, cout, main, is_sock =
+     spawn_with_control prefer_sock env prog args in
+   Unix.set_nonblock (fst main);
+-  let gchan =
+-    if is_sock then ML.async_chan_of_socket (fst main)
+-    else ML.async_chan_of_file (fst main) in
++  let gchan = ML.async_chan_of_file_or_socket (fst main) in
+   let alive, watch = true, None in
+   let p = { cin; cout; gchan; pid; oob_resp; oob_req; alive; watch } in
+   p.watch <- Some (
+diff --git a/lib/spawn.mli b/lib/spawn.mli
+index 34a2cee31b..010eaa48cc 100644
+--- a/lib/spawn.mli
++++ b/lib/spawn.mli
+@@ -43,8 +43,7 @@ module type MainLoopModel = sig
+   val add_watch : callback:(condition list -> bool) -> async_chan -> watch_id
+   val remove_watch : watch_id -> unit
+   val read_all : async_chan -> string
+-  val async_chan_of_file : Unix.file_descr -> async_chan
+-  val async_chan_of_socket : Unix.file_descr -> async_chan
++  val async_chan_of_file_or_socket : Unix.file_descr -> async_chan
+ end
+
+ (* spawn a process and read its output asynchronously *)
+-- 
+2.43.0
+
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
@@ -37,6 +37,10 @@ conflicts: [
 ]
 depopts: ["coq-native" "memprof-limits"]
 dev-repo: "git+https://github.com/coq/coq.git"
+patches: [ 
+  "PR19247-ported-Fix-coqide-compilation-with-lablgtk-3.1.5-on-windows.patch"
+  "0001-Windows-fix-path-normalization-in-coqdep.patch"
+]
 build: [
   ["dune" "subst"] {dev}
   [ "./configure"
@@ -67,3 +71,13 @@ url {
     "sha512=00833a93914d485e6ca695b6cec220da47957d7e3358bfe8e68300c48935255e95436be751826d837dfbd5f784116df86c1b57a8fe7e3301b45b4b19bffe958f"
   ]
 }
+extra-files: [
+  [
+    "0001-Windows-fix-path-normalization-in-coqdep.patch"
+    "sha512=ed520c9e7d17f5bd9067e22d19983571cd88fbae7ae4c62cbc0daac9b607a357224b6e093c962858dd586ccd282d127bac565ed942d7025836e37b6635cbb609"
+  ]
+  [
+    "PR19247-ported-Fix-coqide-compilation-with-lablgtk-3.1.5-on-windows.patch"
+    "sha512=e55c87a7aed663b6c11874e90c2cdc44b4b3d60b525dc3b6b03d40155dadd159414d21fe40a7c4fac8d3adbde67ef787a485c2e54ba417f9ce60439223f58e0d"
+  ]
+]
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
@@ -1,59 +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"
-  ]
+# 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"
+  ]
 }