2 files changed, 25 insertions, 25 deletions
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt
index 052014824f..f34bbea4e9 100644
--- a/dev/build/windows/ReadMe.txt
+++ b/dev/build/windows/ReadMe.txt
@@ -423,7 +423,7 @@ Binary file ./bin/ocpp5.exe matches
 Binary file ./lib/config/coq_config.cmo matches
 Binary file ./lib/config/coq_config.o matches
 Binary file ./lib/grammar/grammar.cma matches
-Binary file ./lib/ide/ide_win32_stubs.o matches
+Binary file ./lib/ide/coqide/ide_win32_stubs.o matches
 Binary file ./lib/lib/clib.a matches
 Binary file ./lib/lib/clib.cma matches
 Binary file ./lib/libcoqrun.a matches
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 963b0e6387..6ceb7f54b2 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1087,11 +1087,10 @@ function make_menhir {
   make_ocaml
   make_findlib
   make_ocamlbuild
-  # This is the version required by latest CompCert
-  if build_prep https://gitlab.inria.fr/fpottier/menhir/-/archive/20190626 menhir-20190626 tar.gz 1 ; then
-    # Note: menhir doesn't support -j 8, so don't pass MAKE_OPT
-    log2 make all PREFIX="$PREFIXOCAML"
-    log2 make install PREFIX="$PREFIXOCAML"
+  if build_prep https://gitlab.inria.fr/fpottier/menhir/-/archive/20200525 menhir-20200525 tar.gz 1 ; then
+    # ToDo: don't know if this is the intended / most reliable to do it, but it works
+    log2 dune build @install
+    log2 dune install menhir menhirSdk menhirLib
     build_post
   fi
 }
@@ -1194,10 +1193,10 @@ function make_elpi {
   make_dune
   make_re
 
-  if build_prep https://github.com/LPCIC/elpi/archive v1.11.0 tar.gz; then
+  if build_prep https://github.com/LPCIC/elpi/archive v1.11.0 tar.gz 1 elpi; then
 
-    log2 make build DUNE_OPTS="-p elpi"
-    log2 make install DUNE_OPTS="-p elpi"
+    log2 dune build -p elpi
+    log2 dune install elpi
 
     build_post
 
@@ -1303,11 +1302,11 @@ function copy_coq_gtk {
     install -D -T "$PREFIXMINGW/share/glib-2.0/schemas/gschemas.compiled"        "$PREFIXCOQ/share/glib-2.0/schemas/gschemas.compiled"
 
     install_glob  "$PREFIXMINGW/share/gtksourceview-3.0/language-specs" '*'      "$PREFIXCOQ/share/gtksourceview-3.0/language-specs"
-    install -D -T "ide/coq.lang"                                                 "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq.lang"
-    install -D -T "ide/coq-ssreflect.lang"                                       "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq-ssreflect.lang"
+    install -D -T "ide/coqide/coq.lang"                                                 "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq.lang"
+    install -D -T "ide/coqide/coq-ssreflect.lang"                                       "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq-ssreflect.lang"
 
     install_glob  "$PREFIXMINGW/share/gtksourceview-3.0/styles" '*'              "$PREFIXCOQ/share/gtksourceview-3.0/styles"
-    install -D -T "ide/coq_style.xml"                                            "$PREFIXCOQ/share/gtksourceview-3.0/styles/coq_style.xml"
+    install -D -T "ide/coqide/coq_style.xml"                                            "$PREFIXCOQ/share/gtksourceview-3.0/styles/coq_style.xml"
 
     install_rec   "$PREFIXMINGW/share/themes" '*'                                "$PREFIXCOQ/share/themes"
 
@@ -1340,8 +1339,8 @@ function copy_coq_gtk {
     #   COQSHARE="$PREFIXCOQ/share/"
     # fi
 
-    # mkdir -p "$PREFIXCOQ/ide"
-    # mv "$COQSHARE"*.png  "$PREFIXCOQ/ide"
+    # mkdir -p "$PREFIXCOQ/ide/coqide"
+    # mv "$COQSHARE"*.png  "$PREFIXCOQ/ide/coqide"
     # rmdir "$PREFIXCOQ/share/coq" || true
   fi
 }
@@ -1598,7 +1597,7 @@ function make_coq_installer {
     cp ../patches/ReplaceInFile.nsh dev/nsis
     VERSION=$(grep '^VERSION=' config/Makefile | cut -d = -f 2 | tr -d '\r')
     cd dev/nsis
-    logn nsis-installer "$NSIS" -DVERSION="$VERSION" -DARCH="$ARCH" -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
+    logn nsis-installer "$NSIS" -DVERSION="$VERSION" -DARCH="$ARCH" -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coqide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
 
     build_post
   fi
@@ -1712,10 +1711,8 @@ function make_addon_menhir {
       touch "$FLAGFILES/menhir-addon.started"
       # Menhir executable
       install_glob "$PREFIXOCAML/bin" 'menhir.exe' "$PREFIXCOQ/bin/"
-      # Menhir Standard library
-      install_glob "$PREFIXOCAML/share/menhir/" '*.mly' "$PREFIXCOQ/share/menhir/"
       # Menhir PDF doc
-      install_glob "$PREFIXOCAML/share/doc/menhir/" '*.pdf' "$PREFIXCOQ/doc/menhir/"
+      install_glob "$PREFIXOCAML/doc/menhir/" '*.pdf' "$PREFIXCOQ/doc/menhir/"
       touch "$FLAGFILES/menhir-addon.finished"
       LOGTARGET=other
       installer_addon_end
@@ -1730,7 +1727,8 @@ function make_addon_menhirlib {
   if build_prep_overlay menhirlib; then
     installer_addon_section menhirlib "Menhirlib" "Coq support library for using Menhir generated parsers in Coq" ""
     # The supplied makefiles don't work in any way on cygwin
-    cd src
+    # ToDo: dune also doesn't seem to work for the coq files
+    cd coq-menhirlib/src
     echo -R . MenhirLib > _CoqProject
     ls -1 *.v >> _CoqProject
     log1 coq_makefile -f _CoqProject -o Makefile.coq
@@ -1816,7 +1814,7 @@ function make_addon_coquelicot {
   installer_addon_dependency_end
   if build_prep_overlay coquelicot; then
     installer_addon_section coquelicot "Coquelicot" "Coq library for real analysis" ""
-    logn autogen ./autogen.sh
+    log1 autoreconf -i -s
     logn configure ./configure --libdir="$PREFIXCOQ/lib/coq/user-contrib/Coquelicot"
     logn remake ./remake
     logn remake-install ./remake install
@@ -1880,9 +1878,9 @@ function make_addon_quickchick {
 # Flocq: Floating point library
 
 function make_addon_flocq {
-  if build_prep_overlay Flocq; then
+  if build_prep_overlay flocq; then
     installer_addon_section flocq "Flocq" "Coq library for floating point arithmetic" ""
-    logn autogen ./autogen.sh
+    log1 autoreconf
     logn configure ./configure
     logn remake ./remake --jobs=$MAKE_THREADS
     logn install ./remake install
@@ -1901,7 +1899,7 @@ function make_addon_interval {
   installer_addon_dependency_end
   if build_prep_overlay interval; then
     installer_addon_section interval "Interval" "Coq library and tactic for proving real inequalities" ""
-    logn autogen ./autogen.sh
+    log1 autoreconf
     logn configure ./configure
     logn remake ./remake --jobs=$MAKE_THREADS
     logn install ./remake install
@@ -1930,7 +1928,9 @@ function make_addon_gappa_tool {
   install_boost
   if build_prep_overlay gappa_tool; then
     installer_addon_section gappa_tool "Gappa tool" "Stand alone tool for automated generation of numerical arithmetic proofs" ""
-    logn autogen ./autogen.sh
+    log1 autoreconf
+    # Note: configure.in seems to reference this file
+    touch stamp-config_h.in
     logn configure ./configure --build="$HOST" --host="$HOST" --target="$TARGET" --prefix="$PREFIXCOQ"
     logn remake ./remake --jobs=$MAKE_THREADS
     logn install ./remake -d install
@@ -1947,7 +1947,7 @@ function make_addon_gappa {
   installer_addon_dependency_end
   if build_prep_overlay gappa_plugin ; then
     installer_addon_section gappa "Gappa plugin" "Coq plugin for the Gappa tool" ""
-    logn autogen ./autogen.sh
+    log1 autoreconf
     logn configure ./configure
     logn remake ./remake
     logn install ./remake install