Windows package fixes

coq_platform_make.sh

@@ -61,6 +61,7 @@ source package_picks/coq_platform_switch_name.sh
 
 source shell_scripts/ask_delete_opam_switch.sh
 source shell_scripts/install_opam.sh
+source shell_scripts/install_ocaml_stacksize.sh
 source shell_scripts/check_opam_sandbox.sh
 source shell_scripts/install_opam_depext.sh
 source shell_scripts/coq_platform_override_dev_pkg.sh

opam/opam-coq-archive/released/packages/coq-mtac2/coq-mtac2.1.4+8.19/files/0001-use-new-way-of-loading-ML-module-makes-Unicoq-module.patch

@@ -0,0 +1,24 @@
+From 211f00876c9d1c8563cf50f94b402cb02ab9d84f Mon Sep 17 00:00:00 2001
+From: Karl Palmskog <[email protected]>
+Date: Wed, 11 Sep 2024 10:13:14 +0200
+Subject: [PATCH] use new way of loading ML module, makes Unicoq module
+ declaration superfluous
+
+---
+ theories/Base.v | 3 +--
+ 1 file changed, 1 insertion(+), 2 deletions(-)
+
+diff --git a/theories/Base.v b/theories/Base.v
+index ae22566..b89da46 100644
+--- a/theories/Base.v
++++ b/theories/Base.v
+@@ -1,5 +1,4 @@
+-Declare ML Module "coq-unicoq.plugin".
+-Declare ML Module "MetaCoqPlugin:coq-mtac2.plugin".
++Declare ML Module "coq-mtac2.plugin".
+
+ (* Declare ML Module must work without the Requires to be compatible
+    with async proofs. Running it before them serves as a test
+-- 
+2.45.1
+

opam/opam-coq-archive/released/packages/coq-mtac2/coq-mtac2.1.4+8.19/opam

@@ -0,0 +1,33 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+homepage: "https://github.com/Mtac2/Mtac2"
+dev-repo: "git+https://github.com/Mtac2/Mtac2.git"
+bug-reports: "https://github.com/Mtac2/Mtac2/issues"
+authors: [
+ "Beta Ziliani <[email protected]>"
+ "Jan-Oliver Kaiser <[email protected]"
+ "Robbert Krebbers <[email protected]>"
+ "Yann Régis-Gianas <[email protected]>"
+]
+license: "MIT"
+synopsis: "Typed tactic language for Coq"
+patches: [
+  "0001-use-new-way-of-loading-ML-module-makes-Unicoq-module.patch" 
+]
+build: [
+  ["./configure.sh"]
+  [make "-j%{jobs}%"]
+]
+install: [
+  [make "install"]
+]
+depends: [
+  "coq" {>= "8.19" & < "8.20"}
+  "coq-unicoq" {>= "1.5" & < "2~"}
+]
+url {
+  src: "https://github.com/Mtac2/Mtac2/archive/refs/tags/v1.4-coq8.19.tar.gz"
+  checksum: [
+    "sha512=4c5f17576bdfa6e127d5901666da640352ad472211bf21cf5ae67944e84ba9bf6306215cfcad83ca2117e29ec40429db8daf7421249e857537a08e827b3c4132"
+  ]
+}

opam/opam-coq-archive/released/packages/coq-quickchick/coq-quickchick.2.0.3/files/0001-Fix-mycppo-script-for-Windows.patch

@@ -0,0 +1,124 @@
+From c6075146a71a399afd66be37878c6947b522bdc1 Mon Sep 17 00:00:00 2001
+From: Li-yao Xia <[email protected]>
+Date: Wed, 21 Aug 2024 11:22:34 +0200
+Subject: [PATCH] Fix mycppo script for Windows
+
+Don't use shebangs, call sh explicitly
+---
+ examples/other/dune |  2 +-
+ plugin/dune         | 14 +++++++-------
+ scripts/dune        |  4 ++--
+ scripts/mk-mycppo   |  7 +++----
+ src/dune            |  8 ++++----
+ 5 files changed, 17 insertions(+), 18 deletions(-)
+ mode change 100755 => 100644 scripts/mk-mycppo
+
+diff --git a/examples/other/dune b/examples/other/dune
+index ea33692a..12ca5f61 100644
+--- a/examples/other/dune
++++ b/examples/other/dune
+@@ -21,5 +21,5 @@
+ (rule
+   (alias compat)
+   (target TacticExampleX.v)
+-  (action (run %{exe:../../scripts/mycppo} %{dep:TacticExampleX.v.cppo} %{target}))
++  (action (run sh %{dep:../../scripts/mycppo} %{dep:TacticExampleX.v.cppo} %{target}))
+   (deps TacticExample.v))
+diff --git a/plugin/dune b/plugin/dune
+index 28e45409..2512d53b 100644
+--- a/plugin/dune
++++ b/plugin/dune
+@@ -38,28 +38,28 @@
+ (rule
+   (alias compat)
+   (target depDriver.ml)
+-  (action (run %{exe:../scripts/mycppo} %{dep:depDriver.ml.cppo} %{target})))
++  (action (run sh %{dep:../scripts/mycppo} %{dep:depDriver.ml.cppo} %{target})))
+ (rule
+   (alias compat)
+   (target genericLib.ml)
+-  (action (run %{exe:../scripts/mycppo} %{dep:genericLib.ml.cppo} %{target})))
++  (action (run sh %{dep:../scripts/mycppo} %{dep:genericLib.ml.cppo} %{target})))
+ (rule
+   (alias compat)
+   (target mergeTypes.ml)
+-  (action (run %{exe:../scripts/mycppo} %{dep:mergeTypes.ml.cppo} %{target})))
++  (action (run sh %{dep:../scripts/mycppo} %{dep:mergeTypes.ml.cppo} %{target})))
+ (rule
+   (alias compat)
+   (target quickChick.mlg)
+-  (action (run %{exe:../scripts/mycppo} %{dep:quickChick.mlg.cppo} %{target})))
++  (action (run sh %{dep:../scripts/mycppo} %{dep:quickChick.mlg.cppo} %{target})))
+ (rule
+   (alias compat)
+   (target tactic_quickchick.mlg)
+-  (action (run %{exe:../scripts/mycppo} %{dep:tactic_quickchick.mlg.cppo} %{target})))
++  (action (run sh %{dep:../scripts/mycppo} %{dep:tactic_quickchick.mlg.cppo} %{target})))
+ (rule
+   (alias compat)
+   (target unifyQC.ml)
+-  (action (run %{exe:../scripts/mycppo} %{dep:unifyQC.ml.cppo} %{target})))
++  (action (run sh %{dep:../scripts/mycppo} %{dep:unifyQC.ml.cppo} %{target})))
+ (rule
+   (alias compat)
+   (target weightmap.mlg)
+-  (action (run %{exe:../scripts/mycppo} %{dep:weightmap.mlg.cppo} %{target})))
++  (action (run sh %{dep:../scripts/mycppo} %{dep:weightmap.mlg.cppo} %{target})))
+diff --git a/scripts/dune b/scripts/dune
+index e8b0861c..648c7946 100644
+--- a/scripts/dune
++++ b/scripts/dune
+@@ -1,3 +1,3 @@
+ (rule
+- (target ./mycppo)
+- (action (run ./mk-mycppo)))
++ (target mycppo)
++ (action (run sh %{dep:mk-mycppo})))
+diff --git a/scripts/mk-mycppo b/scripts/mk-mycppo
+old mode 100755
+new mode 100644
+index 06248650..54b4a216
+--- a/scripts/mk-mycppo
++++ b/scripts/mk-mycppo
+@@ -1,7 +1,6 @@
+-#!/bin/sh
+-# Usage: mycppo input.v.cppo output.v
++# sh mk-mycppo generates the script mycppo
++# Usage: sh mycppo input.v.cppo output.v
+
+ COQVER=$(coqc -print-version)
+ COQVER=${COQVER%% *}
+-printf "#!/bin/sh\ncppo -V OCAML:$(ocamlc -version) -V COQ:$COQVER -n \$1 -o \$2" > mycppo
+-chmod u+x mycppo
++printf "cppo -V OCAML:$(ocamlc -version) -V COQ:$COQVER -n \$1 -o \$2" > mycppo
+diff --git a/src/dune b/src/dune
+index 8fcc3ec0..0505fb00 100644
+--- a/src/dune
++++ b/src/dune
+@@ -6,19 +6,19 @@
+ (rule
+   (alias compat)
+   (target Compat.v)
+-  (action (run %{exe:../scripts/mycppo} %{dep:Compat.v.cppo} %{target})))
++  (action (run sh %{dep:../scripts/mycppo} %{dep:Compat.v.cppo} %{target})))
+
+ (rule
+   (alias compat)
+   (target ExtractionQC.v)
+-  (action (run %{exe:../scripts/mycppo} %{dep:ExtractionQC.v.cppo} %{target})))
++  (action (run sh %{dep:../scripts/mycppo} %{dep:ExtractionQC.v.cppo} %{target})))
+
+ (rule
+   (alias compat)
+   (target QuickChick.v)
+-  (action (run %{exe:../scripts/mycppo} %{dep:QuickChick.v.cppo} %{target})))
++  (action (run sh %{dep:../scripts/mycppo} %{dep:QuickChick.v.cppo} %{target})))
+
+ (rule
+   (alias compat)
+   (target TacticsUtil.v)
+-  (action (run %{exe:../scripts/mycppo} %{dep:TacticsUtil.v.cppo} %{target})))
++  (action (run sh %{dep:../scripts/mycppo} %{dep:TacticsUtil.v.cppo} %{target})))
+-- 
+2.45.1
+

opam/opam-coq-archive/released/packages/coq-quickchick/coq-quickchick.2.0.3/opam

@@ -0,0 +1,45 @@
+opam-version: "2.0"
+synopsis: "Randomized Property-Based Testing for Coq"
+description: """\
+A library for property-based testing in Coq.
+
+  - Combinators for testable properties and random generators.
+  - QuickChick plugin for running tests in a Coq session.
+  - Includes a mutation testing tool."""
+maintainer: "[email protected]"
+authors: [
+  "Leonidas Lampropoulos"
+  "Zoe Paraskevopoulou"
+  "Maxime Denes"
+  "Catalin Hritcu"
+  "Benjamin Pierce"
+  "Li-yao Xia"
+  "Arthur Azevedo de Amorim"
+  "Yishuai Li"
+  "Antal Spector-Zabusky"
+]
+license: "MIT"
+homepage: "https://github.com/QuickChick/QuickChick"
+bug-reports: "https://github.com/QuickChick/QuickChick/issues"
+depends: [
+  "dune" {>= "3.12"}
+  "ocaml" {>= "4.07"}
+  "menhir" {build}
+  "cppo" {build & >= "1.6.8"}
+  "coq" {>= "8.15~" & < "8.21"}
+  "coq-ext-lib"
+  "coq-mathcomp-ssreflect"
+  "coq-simple-io"
+  "ocamlfind"
+  "ocamlbuild"
+]
+patches: [ "0001-Fix-mycppo-script-for-Windows.patch" ]
+build: [
+  ["dune" "subst"] {dev}
+  ["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test}]
+]
+dev-repo: "git+https://github.com/QuickChick/QuickChick.git"
+url {
+  src: "https://github.com/QuickChick/QuickChick/archive/refs/tags/v2.0.3.tar.gz"
+  checksum: "sha512=0857dc53fb3c98d596d6464df07d9a6426dbf587f639ea5e87200d161b03aad6d9ce429ecffe3e93b010ac22d616f95922154571553ba238e23d7eb08ee75472"
+}

package_picks/package-pick-8.19~2024.01+beta1.sh

@@ -126,10 +126,7 @@ then
   PACKAGES="${PACKAGES} coq-equations.1.3+8.19"
   PACKAGES="${PACKAGES} coq-aac-tactics.8.19.0"
   PACKAGES="${PACKAGES} coq-unicoq.1.6+8.19"
-  if [[ "$OSTYPE" != cygwin ]]
-  then
-    PACKAGES="${PACKAGES} coq-mtac2.1.4+8.19" # build issues on Windows
-  fi
+  PACKAGES="${PACKAGES} coq-mtac2.1.4+8.19" # build issues on Windows
   PACKAGES="${PACKAGES} elpi.1.18.2 coq-elpi.2.1.0"
   PACKAGES="${PACKAGES} coq-hierarchy-builder.1.7.0"
   if [[ "$OSTYPE" != cygwin ]]
@@ -158,13 +155,8 @@ then
   PACKAGES="${PACKAGES} coq-reglang.1.2.1"
   PACKAGES="${PACKAGES} coq-iris.4.2.0"
   PACKAGES="${PACKAGES} coq-iris-heap-lang.4.2.0"
-  if [[ "$OSTYPE" != cygwin ]]
-  then
-    # Windows: some issues with executable extensions (ott.opt instead of ott.exe)
-    # Note: 0.32 does work on Windows!
-    PACKAGES="${PACKAGES} coq-ott.0.33"
-    PACKAGES="${PACKAGES} ott.0.33"
-  fi
+  PACKAGES="${PACKAGES} coq-ott.0.33"
+  PACKAGES="${PACKAGES} ott.0.33"
   PACKAGES="${PACKAGES} coq-mathcomp-word.3.0"
 
   case "$COQ_PLATFORM_COMPCERT" in
@@ -218,12 +210,7 @@ then
         PACKAGES="${PACKAGES} coq-bedrock2.0.0.7"
         PACKAGES="${PACKAGES} coq-bedrock2-compiler.0.0.7"
         PACKAGES="${PACKAGES} coq-rupicola.0.0.9"
-        if [ "$OSTYPE" != cygwin ]
-        then
-          # Windows: stack overflow
-          PACKAGES="${PACKAGES} coq-fiat-crypto.0.1.2"
-          true
-        fi
+        PACKAGES="${PACKAGES} coq-fiat-crypto.0.1.2"
         ;;
       [nN]) true ;;
       *) echo "Illegal value for COQ_PLATFORM_FIATCRYPTO - aborting"; false ;;

shell_scripts/install_ocaml_stacksize.sh

@@ -0,0 +1,42 @@
+#!/bin/bash
+
+###################### COPYRIGHT/COPYLEFT ######################
+
+# (C) 2020 Michael Soegtrop
+
+# Released to the public under the
+# Creative Commons CC0 1.0 Universal License
+# See https://creativecommons.org/publicdomain/zero/1.0/legalcode.txt
+
+###################### Set ocamlc stack size on Windows #####################
+
+DUMPBIN='C:/Program Files/Microsoft Visual Studio/2022/Professional/VC/Tools/MSVC/14.41.34120/bin/Hostx64/x64/dumpbin.exe'
+
+function show_stack_size {
+    # If dumpbin exists, we use it to check the operation of our set_stack_size program
+    if [ -f "$DUMPBIN" ]
+    then
+        "$DUMPBIN" /HEADERS "$1" | grep "size of stack reserve"
+    fi
+}
+
+function do_set_stack_size {
+    echo "Setting stack size of $1 to $2"
+    show_stack_size "$1"
+    ./set_stack_size.exe "$1" "$2"
+    show_stack_size "$1"
+}
+
+if [[ "$OSTYPE" == cygwin ]]
+then
+    pushd windows/set_stack_size
+    ocamlopt -o set_stack_size unix.cmxa set_stack_size.ml
+    do_set_stack_size "$(cygpath -aw $(which ocamlc.exe))" 67108864
+    do_set_stack_size "$(cygpath -aw $(which ocamlc.opt.exe))" 67108864
+    do_set_stack_size "$(cygpath -aw $(which ocamlopt.exe))" 67108864
+    do_set_stack_size "$(cygpath -aw $(which ocamlopt.opt.exe))" 67108864
+    # do_set_stack_size "$(cygpath -aw $(which coqc.exe))" 67108864
+    # do_set_stack_size "$(cygpath -aw $(which coqnative.exe))" 67108864
+    # do_set_stack_size "$(cygpath -aw $(which coqidetop.opt.exe))" 67108864
+    popd
+fi

windows/set_stack_size/dune

@@ -0,0 +1,3 @@
+(executable
+ (name set_stack_size)
+ (libraries unix))

windows/set_stack_size/dune-project

@@ -0,0 +1,4 @@
+(lang dune 3.15)
+(name set_stack_size)
+
+; See the complete stanza docs at https://dune.readthedocs.io/en/stable/dune-files.html#dune-project

windows/set_stack_size/set_stack_size.ml

@@ -0,0 +1,55 @@
+(* See https://discuss.ocaml.org/t/how-to-set-the-stacksize-for-ocamlopt-opt-exe-on-mingw-cygwin-host/15279 *)
+
+(* Modify the stack size of the resulting PE executable.
+
+  See https://learn.microsoft.com/en-us/windows/win32/debug/pe-format for a
+  description of the PE format. *)
+
+let perform ~__FUNCTION__ f fd ofs len buf =
+  if Bytes.length buf < len then invalid_arg __FUNCTION__;
+  let _ = Unix.lseek fd ofs SEEK_SET in
+  let rec loop ofs len =
+    if len <= 0 then ()
+    else begin
+      let n = f fd buf ofs len in
+      if n = 0 then raise End_of_file;
+      loop (ofs + n) (len - n)
+    end
+  in
+  loop 0 len
+
+let really_read = perform ~__FUNCTION__ Unix.read
+let really_write = perform ~__FUNCTION__ Unix.write
+
+let read_bytes fd ofs len =
+  let buf = Bytes.create len in
+  really_read fd ofs len buf;
+  Bytes.unsafe_to_string buf
+
+let read_int f len fd ofs =
+  f (read_bytes fd ofs len) 0
+
+let read_int32 = read_int String.get_int32_le 4
+let read_int16 = read_int String.get_int16_le 2
+
+let write_int f len =
+  let buf = Bytes.create len in
+  fun fd ofs n ->
+    f buf 0 n;
+    really_write fd ofs len buf
+
+let write_int64 = write_int Bytes.set_int64_le 8
+
+let set_stack_size out n =
+  assert (Sys.word_size = 64);
+  let fd = Unix.openfile out [O_RDWR; O_SHARE_DELETE] 0o755 in
+  let base = Option.get (Int32.unsigned_to_int (read_int32 fd 0x3c)) in
+  let sign = read_bytes fd base 4 in
+  if sign <> "PE\000\000" then Printf.ksprintf failwith "Invalid PE Signature: %S" sign;
+  let base = base + 24 in
+  let sign = read_int16 fd base in
+  if sign <> 0x20b then Printf.ksprintf failwith "Invalid PE Optional Header Signature: 0x%x" sign;
+  write_int64 fd (base + 72) n
+
+let _ = set_stack_size (Sys.argv.(1)) (Int64.of_string Sys.argv.(2))
+;;