aboutsummaryrefslogtreecommitdiff
path: root/dev/build
diff options
context:
space:
mode:
Diffstat (limited to 'dev/build')
-rwxr-xr-xdev/build/osx/make-macos-dmg.sh7
-rw-r--r--dev/build/windows/MakeCoq_MinGW.bat23
-rw-r--r--dev/build/windows/MakeCoq_regtest_noproxy.bat4
-rw-r--r--dev/build/windows/appveyor.sh8
-rw-r--r--dev/build/windows/configure_profile.sh2
-rw-r--r--dev/build/windows/makecoq_mingw.sh35
-rw-r--r--dev/build/windows/patches_coq/ln.c2
7 files changed, 40 insertions, 41 deletions
diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh
index cbe2a5186f..cfcc09b327 100755
--- a/dev/build/osx/make-macos-dmg.sh
+++ b/dev/build/osx/make-macos-dmg.sh
@@ -9,15 +9,12 @@ DMGDIR=$PWD/_dmg
VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml)
APP=bin/CoqIDE_${VERSION}.app
-# Create a .app file with CoqIDE
-make -j $NJOBS -l2 $APP
+# Create a .app file with CoqIDE, without signing it
+make PRIVATEBINARIES=$APP -j $NJOBS -l2 $APP
# Add Coq to the .app file
make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq install-ide-toploop
-# Sign the .app file
-codesign -f -s - $APP
-
# Create the dmg bundle
mkdir -p $DMGDIR
ln -sf /Applications $DMGDIR/Applications
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index b2efe2ddd4..f91b301b8c 100644
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -328,12 +328,6 @@ ECHO ========== INSTALL CYGWIN ==========
REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
REM Otherwise chmod won't work and e.g. the ocaml build will fail.
REM Cygwin setup does not touch the ACLs of existing folders.
-REM => Create the setup log in a temporary location and move it later.
-
-REM Get Unique temporary file name
-:logfileloop
-SET LOGFILE=%TEMP%\CygwinSetUp%RANDOM%-%RANDOM%-%RANDOM%-%RANDOM%.log
-if exist "%LOGFILE%" GOTO logfileloop
REM Run Cygwin Setup
@@ -344,6 +338,15 @@ IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" (
IF NOT "%CYGWIN_QUIET%" == "Y" (
SET RUNSETUP=Y
)
+IF "%COQREGTESTING%" == "Y" (
+ SET RUNSETUP=Y
+)
+
+SET "EXTRAPACKAGES= "
+
+IF NOT "%APPVEYOR%" == "True" (
+ SET EXTRAPACKAGES="-P wget,curl,git,gcc-core,gcc-g++,automake1.5"
+)
IF "%RUNSETUP%"=="Y" (
%SETUP% ^
@@ -353,10 +356,9 @@ IF "%RUNSETUP%"=="Y" (
--local-package-dir "%CYGWIN_LOCAL_CACHE_WFMT%" ^
--no-shortcuts ^
%CYGWIN_OPT% ^
- -P wget,curl,git,make,unzip ^
- -P gcc-core,gcc-g++ ^
+ -P make,unzip ^
-P gdb,liblzma5 ^
- -P patch,automake1.14,automake1.15 ^
+ -P patch,automake1.14 ^
-P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-pkg-config,mingw64-%ARCH%-windows_default_manifest ^
-P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
-P libiconv-devel,libunistring-devel,libncurses-devel ^
@@ -366,12 +368,11 @@ IF "%RUNSETUP%"=="Y" (
-P gtk-update-icon-cache ^
-P libtool,automake ^
-P intltool ^
- > "%LOGFILE%" ^
+ %EXTRAPACKAGES% ^
|| GOTO ErrorExit
MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs"
- MOVE "%LOGFILE%" "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs\cygwinsetup.log" || GOTO ErrorExit
)
diff --git a/dev/build/windows/MakeCoq_regtest_noproxy.bat b/dev/build/windows/MakeCoq_regtest_noproxy.bat
index 7b17e721b3..7140a7c619 100644
--- a/dev/build/windows/MakeCoq_regtest_noproxy.bat
+++ b/dev/build/windows/MakeCoq_regtest_noproxy.bat
@@ -25,5 +25,5 @@ call MakeCoq_MinGW.bat ^
-cygquiet=Y ^
-destcyg %ROOTPATH%\cygwin_coq64_85pl2_abs ^
-destcoq %ROOTPATH%\coq64_85pl2_abs
-
-pause \ No newline at end of file
+
+pause
diff --git a/dev/build/windows/appveyor.sh b/dev/build/windows/appveyor.sh
deleted file mode 100644
index 53f7a23466..0000000000
--- a/dev/build/windows/appveyor.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/bin/bash
-set -e -x
-wget $opam_url
-tar -xf opam64.tar.xz
-bash opam64/install.sh
-opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c
-eval $(opam config env)
-opam install -y ocamlfind camlp5
diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh
index 0b61a31e7f..16c972e80c 100644
--- a/dev/build/windows/configure_profile.sh
+++ b/dev/build/windows/configure_profile.sh
@@ -40,4 +40,4 @@ if [ ! -f $donefile ] ; then
echo unset OCAMLLIB >> $rcfile
touch $donefile
-fi \ No newline at end of file
+fi
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index e179239514..f12cbe0a78 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -910,6 +910,10 @@ function make_camlp5 {
log2 make install
# For some reason gramlib.a is not copied, but it is required by Coq
cp lib/gramlib.a "$PREFIXOCAML/libocaml/camlp5/"
+ # For some reason META is not copied, but it is required by coq_makefile
+ log2 make -C etc META
+ mkdir -p "$PREFIXOCAML/libocaml/site-lib/camlp5/"
+ cp etc/META "$PREFIXOCAML/libocaml/site-lib/camlp5/"
log2 make clean
build_post
fi
@@ -1058,13 +1062,18 @@ function copq_coq_gtk {
install_rec "$PREFIX/share/themes/" '*' "$PREFIXCOQ/share/themes"
# This below item look like a bug in make install
+ if [ -d "$PREFIXCOQ/share/coq/" ] ; then
+ COQSHARE="$PREFIXCOQ/share/coq/"
+ else
+ COQSHARE="$PREFIXCOQ/share/"
+ fi
if [[ ! $COQ_VERSION == 8.4* ]] ; then
- mv "$PREFIXCOQ/share/coq/"*.lang "$PREFIXCOQ/share/gtksourceview-2.0/language-specs"
- mv "$PREFIXCOQ/share/coq/"*.xml "$PREFIXCOQ/share/gtksourceview-2.0/styles"
+ mv "$COQSHARE"*.lang "$PREFIXCOQ/share/gtksourceview-2.0/language-specs"
+ mv "$COQSHARE"*.xml "$PREFIXCOQ/share/gtksourceview-2.0/styles"
fi
mkdir -p "$PREFIXCOQ/ide"
- mv "$PREFIXCOQ/share/coq/"*.png "$PREFIXCOQ/ide"
- rmdir "$PREFIXCOQ/share/coq"
+ mv "$COQSHARE"*.png "$PREFIXCOQ/ide"
+ rmdir "$PREFIXCOQ/share/coq" || true
fi
}
@@ -1119,11 +1128,11 @@ function make_coq {
then
if [ "$INSTALLMODE" == "relocatable" ]; then
# HACK: for relocatable builds, first configure with ./, then build but before install reconfigure with the real target path
- logn configure ./configure -debug -with-doc no -prefix ./ -libdir ./lib -mandir ./man
+ ./configure -with-doc no -prefix ./ -libdir ./lib -mandir ./man
elif [ "$INSTALLMODE" == "absolute" ]; then
- logn configure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
+ ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
else
- logn configure ./configure -debug -with-doc no -prefix "$PREFIXCOQ"
+ ./configure -with-doc no -prefix "$PREFIXCOQ"
fi
# The windows resource compiler binary name is hard coded
@@ -1134,17 +1143,17 @@ function make_coq {
if [[ $COQ_VERSION == 8.4* ]] ; then
log1 make
else
- log1 make $MAKE_OPT
+ make $MAKE_OPT
fi
if [ "$INSTALLMODE" == "relocatable" ]; then
- logn reconfigure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
+ ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
fi
- log2 make install
- log1 copy_coq_dlls
+ make install
+ copy_coq_dlls
if [ "$INSTALLOCAML" == "Y" ]; then
- log1 copy_coq_objects
+ copy_coq_objects
fi
copq_coq_gtk
@@ -1267,7 +1276,7 @@ function get_cygwin_mingw_sources {
function make_coq_installer {
make_coq
make_mingw_make
- # get_cygwin_mingw_sources
+ get_cygwin_mingw_sources
# Prepare the file lists for the installer. We created to file list dumps of the target folder during the build:
# ocaml: ocaml + menhir + camlp5 + findlib
diff --git a/dev/build/windows/patches_coq/ln.c b/dev/build/windows/patches_coq/ln.c
index 5e02c72bb7..41f64f98b2 100644
--- a/dev/build/windows/patches_coq/ln.c
+++ b/dev/build/windows/patches_coq/ln.c
@@ -134,4 +134,4 @@ int WINAPI WinMain( HINSTANCE hInstance, HINSTANCE hPrevInstance, LPSTR lpCmdLin
// Everything is fine
return 0;
-} \ No newline at end of file
+}
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 16:55:06 +0000