aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/base_include7
-rw-r--r--dev/build/windows/MakeCoq_MinGW.bat13
-rw-r--r--dev/build/windows/ReadMe.txt5
-rw-r--r--dev/build/windows/makecoq_mingw.sh39
-rw-r--r--dev/build/windows/patches_coq/coq_new.nsi11
-rw-r--r--dev/ci/appveyor.bat1
-rw-r--r--dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh7
-rw-r--r--dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh6
-rw-r--r--dev/doc/build-system.txt4
-rw-r--r--dev/doc/setup.txt10
-rw-r--r--dev/header.c9
-rw-r--r--dev/header.ml (renamed from dev/header)0
-rw-r--r--dev/header.py9
-rwxr-xr-xdev/lint-commits.sh19
-rw-r--r--dev/top_printers.ml18
-rw-r--r--dev/top_printers.mli10
-rw-r--r--dev/vm_printers.ml7
17 files changed, 145 insertions, 30 deletions
diff --git a/dev/base_include b/dev/base_include
index 350ccaa109..3320a2a942 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -196,7 +196,10 @@ let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
(* build a term of type glob_constr without type-checking or resolution of
implicit syntax *)
-let e s = Constrintern.intern_constr (Global.env()) (parse_constr s);;
+let e s =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Constrintern.intern_constr env sigma (parse_constr s);;
(* build a term of type constr with type-checking and resolution of
implicit syntax *)
@@ -229,7 +232,7 @@ let _ = Flags.in_toplevel := true
let _ = Constrextern.set_extern_reference
(fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));;
-let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqtop.drop_last_doc)
+let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqloop.drop_last_doc)
let _ =
print_string
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index 665d541761..ccf22cc866 100644
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -78,6 +78,9 @@ SET GTK_FROM_SOURCES=N
REM see -threads in ReadMe.txt
SET MAKE_THREADS=8
+REM see -addon in ReadMe.txt
+SET "COQ_ADDONS= "
+
REM ========== PARSE COMMAND LINE PARAMETERS ==========
SHIFT
@@ -233,6 +236,14 @@ IF "%~0" == "-threads" (
GOTO Parse
)
+IF "%~0" == "-addon" (
+ SET "COQ_ADDONS=%COQ_ADDONS% %~1"
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+
IF NOT "%~0" == "" (
ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW
ECHO !!! Illegal parameter %~0
@@ -426,6 +437,7 @@ ECHO ========== BATCH FUNCTIONS ==========
ECHO -coqver ^<Coq version to install^>
ECHO -gtksrc ^<Y or N^> build GTK ^(90 min^) or use cygwin version
ECHO -threads ^<1..N^> Number of make threads
+ ECHO -addon ^<name^> Enable building selected addon (can be repeated)
ECHO(
ECHO See ReadMe.txt for a detailed description of all parameters
ECHO(
@@ -447,6 +459,7 @@ ECHO ========== BATCH FUNCTIONS ==========
ECHO -coqver = %COQ_VERSION%
ECHO -gtksrc = %GTK_FROM_SOURCES%
ECHO -threads = %MAKE_THREADS%
+ ECHO -addon = %COQ_ADDONS%
GOTO :EOF
:CheckYN
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt
index 7e80e33c6d..93851aeb8d 100644
--- a/dev/build/windows/ReadMe.txt
+++ b/dev/build/windows/ReadMe.txt
@@ -61,6 +61,7 @@ The Script MakeCoq_MinGW does:
- either installs MinGW GTK via Cygwin or compiles it fom sources
- download, compile and install OCaml, CamlP5, Menhir, lablgtk
- download, compile and install Coq
+- download, compile and install selected addons
- create a Windows installer (NSIS based)
The parameters are described below. Mostly paths and the HTTP proxy need to be
@@ -335,6 +336,10 @@ Possible values: 1..N.
Should not be more than 1.5x the number of cores.
Should not be more than available RAM/2GB (e.g. 4 for 8GB)
+===== -addon =====
+
+Enable build and installation of selected Coq package (can be repeated for
+selecting more packages)
==================== TODO ====================
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index d8cde39f82..bea30b1a72 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -223,6 +223,12 @@ function get_expand_source_tar {
cp "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" $TARBALLS
else
wget $1/$2.$3
+ if file -i $2.$3 | grep text/html; then
+ echo Download failed: $1/$2.$3
+ echo The file wget downloaded is an html file:
+ cat $2.$3
+ exit 1
+ fi
if [ ! "$2.$3" == "$name.$3" ] ; then
mv $2.$3 $name.$3
fi
@@ -1280,7 +1286,8 @@ function make_coq_installer {
# 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
- # ocal_coq: as above + coq
+ # ocaml_coq: as above + coq
+ # ocaml_coq_addons: as above + lib/user-contrib/*
# Create coq file list as ocaml_coq / ocaml
diff_files coq ocaml_coq ocaml
@@ -1294,11 +1301,17 @@ function make_coq_installer {
# Coq objects objects required for plugin development = coq objects except those for pre installed plugins
diff_files coq_plugindev coq_objects coq_objects_plugins
+ # Addons (TODO: including objects that could go to the plugindev thing, but
+ # then one would have to make that package depend on this one, so not
+ # implemented yet)
+ diff_files coq_addons ocaml_coq_addons ocaml_coq
+
# Coq files, except objects needed only for plugin development
diff_files coq_base coq coq_plugindev
# Convert section files to NSIS format
files_to_nsis coq_base
+ files_to_nsis coq_addons
files_to_nsis coq_plugindev
files_to_nsis ocaml
@@ -1314,12 +1327,30 @@ 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 coq_new.nsi
+ logn nsis-installer "$NSIS" -DVERSION=$VERSION -DARCH=$ARCH -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
build_post
fi
}
+###################### ADDONS #####################
+
+function make_addon_bignums {
+ if build_prep https://github.com/coq/bignums/archive/ master zip 1 bignums-8.8.0; then
+ # To make command lines shorter :-(
+ echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local
+ logn make make all
+ logn make-install make install
+ build_post
+ fi
+}
+
+function make_addons {
+ for addon in $COQ_ADDONS; do
+ make_addon_$addon
+ done
+}
+
###################### TOP LEVEL BUILD #####################
make_sed
@@ -1337,6 +1368,10 @@ fi
list_files ocaml_coq
+make_addons
+
+list_files ocaml_coq_addons
+
if [ "$MAKEINSTALLER" == "Y" ] ; then
make_coq_installer
fi
diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi
index 2c2f0fa47c..55fba6d5ab 100644
--- a/dev/build/windows/patches_coq/coq_new.nsi
+++ b/dev/build/windows/patches_coq/coq_new.nsi
@@ -9,6 +9,7 @@
; ARCH The target architecture, either x86_64 or i686
; COQ_SRC_PATH path of Coq installation in Windows or MinGW format (either \\ or /, but with drive letter)
; COQ_ICON path of Coq icon file in Windows or MinGW format
+; COQ_ADDONS list of addons that are shipped
; Enable compression after debugging.
; SetCompress off
@@ -69,7 +70,8 @@ Var INSTDIR_DBS ; INSTDIR with \\ instead of \
;Description
LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE."
- LangString DESC_2 ${LANG_ENGLISH} "This package contains an OCaml compiler for Coq native compute and plugin development."
+ LangString DESC_2 ${LANG_ENGLISH} "This package contains the following extra Coq packages: ${COQ_ADDONS}"
+ ;LangString DESC_2 ${LANG_ENGLISH} "This package contains an OCaml compiler for Coq native compute and plugin development."
LangString DESC_3 ${LANG_ENGLISH} "This package contains the development files needed in order to build a plugin for Coq."
LangString DESC_4 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for the current user."
LangString DESC_5 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for all users."
@@ -150,6 +152,11 @@ SectionEnd
;OCAML !insertmacro ReplaceInFile "$INSTDIR\etc\findlib.conf" "$COQ_SRC_PATH_DBS" "$INSTDIR_DBS"
;OCAML SectionEnd
+Section "Coq packages" Sec2
+ SetOutPath "$INSTDIR\"
+ !include "..\..\..\filelists\coq_addons.nsh"
+SectionEnd
+
Section "Coq files for plugin developers" Sec3
SetOutPath "$INSTDIR\"
!include "..\..\..\filelists\coq_plugindev.nsh"
@@ -176,7 +183,7 @@ SectionEnd
!insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN
!insertmacro MUI_DESCRIPTION_TEXT ${Sec1} $(DESC_1)
- ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2)
+ !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2)
!insertmacro MUI_DESCRIPTION_TEXT ${Sec3} $(DESC_3)
;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec4} $(DESC_4)
;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec5} $(DESC_5)
diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat
index dec6f0d182..85a71baf7f 100644
--- a/dev/ci/appveyor.bat
+++ b/dev/ci/appveyor.bat
@@ -23,6 +23,7 @@ if %USEOPAM% == false (
call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^
-destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
+ -addon=bignums -make=N ^
-setup %CYGROOT%\%SETUP% || GOTO ErrorExit
copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit
7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
diff --git a/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh b/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh
new file mode 100644
index 0000000000..4b681909d6
--- /dev/null
+++ b/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh
@@ -0,0 +1,7 @@
+ if [ "$CI_PULL_REQUEST" = "6511" ] || [ "$CI_BRANCH" = "econstr+more_fix" ]; then
+ ltac2_CI_BRANCH=econstr+more_fix
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ Equations_CI_BRANCH=econstr+more_fix
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+fi
diff --git a/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh b/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh
new file mode 100644
index 0000000000..2451657d43
--- /dev/null
+++ b/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "6676" ] || [ "$CI_BRANCH" = "proofview/goal-w-state" ]; then
+ ltac2_CI_BRANCH=fix-for/6676
+ ltac2_CI_GITURL=https://github.com/gares/ltac2.git
+ Equations_CI_BRANCH=fix-for/6676
+ Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git
+fi
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 1c4fd2eba4..fd3101613a 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -143,7 +143,9 @@ file list(s):
These files are also used by the experimental ocamlbuild plugin,
which is quite touchy about them : be careful with order,
duplicated entries, whitespace errors, and do not mention .mli there.
- - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
+ If module B depends on module A, then B should be after A in the .mllib
+ file.
+- For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
- The definitions in Makefile.common might have to be adapted too.
- If your file needs a specific rule, add it to Makefile.build
diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt
index 0003a2c217..c48c2d5d16 100644
--- a/dev/doc/setup.txt
+++ b/dev/doc/setup.txt
@@ -41,15 +41,15 @@ Building coqtop:
cd ~/git/coq
git checkout trunk
make distclean
- ./configure -annotate -local
+ ./configure -profile devel
make clean
make -j4 coqide printers
-The "-annotate" option is essential when one wants to use Merlin.
+The "-profile devel" enables all options recommended for developers (like
+warnings, support for Merlin, etc). Moreover Coq is configured so that
+it can be run without installing it (i.e. from the current directory).
-The "-local" option is useful if one wants to run the coqtop and coqide binaries without running make install
-
-Then check if
+Once the compilation is over check if
- bin/coqtop
- bin/coqide
behave as expected.
diff --git a/dev/header.c b/dev/header.c
new file mode 100644
index 0000000000..663c43b3d6
--- /dev/null
+++ b/dev/header.c
@@ -0,0 +1,9 @@
+/************************************************************************/
+/* * The Coq Proof Assistant / The Coq Development Team */
+/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */
+/* <O___,, * (see CREDITS file for the list of authors) */
+/* \VV/ **************************************************************/
+/* // * This file is distributed under the terms of the */
+/* * GNU Lesser General Public License Version 2.1 */
+/* * (see LICENSE file for the text of the license) */
+/************************************************************************/
diff --git a/dev/header b/dev/header.ml
index 7c3ee60040..7c3ee60040 100644
--- a/dev/header
+++ b/dev/header.ml
diff --git a/dev/header.py b/dev/header.py
new file mode 100644
index 0000000000..f81c8aa6a2
--- /dev/null
+++ b/dev/header.py
@@ -0,0 +1,9 @@
+##########################################################################
+## # The Coq Proof Assistant / The Coq Development Team ##
+## v # INRIA, CNRS and contributors - Copyright 1999-2018 ##
+## <O___,, # (see CREDITS file for the list of authors) ##
+## \VV/ ###############################################################
+## // # This file is distributed under the terms of the ##
+## # GNU Lesser General Public License Version 2.1 ##
+## # (see LICENSE file for the text of the license) ##
+##########################################################################
diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh
index eb12bc2273..d8043558eb 100755
--- a/dev/lint-commits.sh
+++ b/dev/lint-commits.sh
@@ -19,14 +19,21 @@ fi
BASE_COMMIT="$1"
HEAD_COMMIT="$2"
-# git diff --check
-# uses .gitattributes to know what to check
-if git diff --check "$BASE_COMMIT" "$HEAD_COMMIT";
+bad=()
+while IFS= read -r commit; do
+ echo Checking "$commit"
+ # git diff --check
+ # uses .gitattributes to know what to check
+ if ! git diff --check "${commit}^" "$commit";
+ then
+ bad+=("$commit")
+ fi
+done < <(git rev-list "$HEAD_COMMIT" --not "$BASE_COMMIT" --)
+
+if [ "${#bad[@]}" != 0 ]
then
- :
-else
>&2 echo "Whitespace errors!"
- >&2 echo "Running 'git diff --check $BASE_COMMIT $HEAD_COMMIT'."
+ >&2 echo "In commits ${bad[*]}"
>&2 echo "If you use emacs, you can prevent this kind of error from reocurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces."
exit 1
fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f99e2593d7..74cdd788b4 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* Printers for the ocaml toplevel. *)
@@ -313,6 +315,8 @@ let constr_display csr =
in
pp (str (term_display csr) ++fnl ())
+let econstr_display c = constr_display EConstr.Unsafe.(to_constr c) ;;
+
open Format;;
let print_pure_constr csr =
@@ -452,6 +456,8 @@ let print_pure_constr csr =
print_string (Printexc.to_string e);print_flush ();
raise e
+let print_pure_econstr c = print_pure_constr EConstr.Unsafe.(to_constr c) ;;
+
let pploc x = let (l,r) = Loc.unloc x in
print_string"(";print_int l;print_string",";print_int r;print_string")"
@@ -505,7 +511,7 @@ let _ =
(function
[c] when genarg_tag c = unquote (topwit wit_constr) && true ->
let c = out_gen (rawwit wit_constr) c in
- (fun ~atts ~st -> in_current_context constr_display c; st)
+ (fun ~atts ~st -> in_current_context econstr_display c; st)
| _ -> failwith "Vernac extension: cannot occur")
with
e -> pp (CErrors.print e)
@@ -521,7 +527,7 @@ let _ =
(function
[c] when genarg_tag c = unquote (topwit wit_constr) && true ->
let c = out_gen (rawwit wit_constr) c in
- (fun ~atts ~st -> in_current_context print_pure_constr c; st)
+ (fun ~atts ~st -> in_current_context print_pure_econstr c; st)
| _ -> failwith "Vernac extension: cannot occur")
with
e -> pp (CErrors.print e)
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 7b5e4a0b64..e47be638aa 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Printers for the ocaml toplevel. *)
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index f819d2e6a9..2ddf927d9b 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -36,6 +36,10 @@ let print_idkey idk =
print_string ")"
| VarKey id -> print_string (Id.to_string id)
| RelKey i -> print_string "~";print_int i
+ | EvarKey evk ->
+ print_string "Evar(";
+ print_int (Evar.repr evk);
+ print_string ")"
let rec ppzipper z =
match z with
@@ -61,7 +65,7 @@ and ppstack s =
and ppatom a =
match a with
| Aid idk -> print_idkey idk
- | Atype u -> print_string "Type(...)"
+ | Asort u -> print_string "Sort(...)"
| Aind(sp,i) -> print_string "Ind(";
print_string (MutInd.to_string sp);
print_string ","; print_int i;
@@ -69,7 +73,6 @@ and ppatom a =
and ppwhd whd =
match whd with
- | Vsort s -> ppsort s
| Vprod _ -> print_string "product"
| Vfun _ -> print_string "function"
| Vfix _ -> print_vfix()
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 03:03:06 +0000