diff options
Diffstat (limited to 'dev')
31 files changed, 427 insertions, 74 deletions
diff --git a/dev/README b/dev/README index 6b83579def..453f85f0d6 100644 --- a/dev/README +++ b/dev/README @@ -40,7 +40,11 @@ Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) Other development tools (directory tools) ----------------------- +coqdev.el: helper customizations for everyday Coq development, eg + making `compile' work in subdirectories + objects.el: various development utilities at emacs level + anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from the Emacs *compilation* output. diff --git a/dev/base_include b/dev/base_include index 472c0c605e..3320a2a942 100644 --- a/dev/base_include +++ b/dev/base_include @@ -19,7 +19,6 @@ #directory "stm";; #directory "vernac";; -#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) #directory "+camlp5";; (* Gramext is found in top_printers.ml *) #use "top_printers.ml";; @@ -197,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 *) @@ -230,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 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 c467678215..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 @@ -794,8 +800,8 @@ function make_ocaml { # TODO: this might not work if PREFIX contains spaces sed -i "s|^PREFIX=.*|PREFIX=$PREFIXOCAML|" config/Makefile - # We don't want to mess up Coq's dirctory structure so put the OCaml library in a separate folder - # If we refer to the make variable ${PREFIX} below, camlp4 ends up having a wrong path: + # We don't want to mess up Coq's directory structure so put the OCaml library in a separate folder + # If we refer to the make variable ${PREFIX} below, camlp5 ends up having the wrong path: # D:\bin\coq64_buildtest_abs_ocaml4\bin>ocamlc -where => D:/bin/coq64_buildtest_abs_ocaml4/libocaml # D:\bin\coq64_buildtest_abs_ocaml4\bin>camlp4 -where => ${PREFIX}/libocaml\camlp4 # So we put an explicit path in there @@ -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/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 784da6f971..48e01e9e93 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -144,3 +144,9 @@ ######################################################################## : "${Equations_CI_BRANCH:=8.8+alpha}" : "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}" + +######################################################################## +# Elpi +######################################################################## +: "${Elpi_CI_BRANCH:=coq-master}" +: "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi.git}" diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh new file mode 100755 index 0000000000..c44e0a6552 --- /dev/null +++ b/dev/ci/ci-elpi.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +Elpi_CI_DIR=${CI_BUILD_DIR}/elpi + +git_checkout ${Elpi_CI_BRANCH} ${Elpi_CI_GITURL} ${Elpi_CI_DIR} + +( cd ${Elpi_CI_DIR} && make && make install ) 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/ci/user-overlays/06745-ejgallego-located+vernac.sh b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh new file mode 100644 index 0000000000..d1d61fec2e --- /dev/null +++ b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh @@ -0,0 +1,13 @@ +if [ "$CI_PULL_REQUEST" = "6745" ] || [ "$CI_BRANCH" = "located+vernac" ]; then + ltac2_CI_BRANCH=located+vernac + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Equations_CI_BRANCH=located+vernac + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + fiat_parsers_CI_BRANCH=located+vernac + fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat + + Elpi_CI_BRANCH=located+vernac + Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git +fi diff --git a/dev/core.dbg b/dev/core.dbg index 00a4355a48..57c136900d 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -1,4 +1,4 @@ -source camlp4.dbg +source camlp5.dbg load_printer threads.cma load_printer str.cma load_printer clib.cma diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index f3fc13e969..abba13428f 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -46,7 +46,7 @@ see build-system.txt . .ml4 files ---------- -.ml4 are converted to .ml by camlp4. By default, they are produced +.ml4 are converted to .ml by camlp5. By default, they are produced in the binary ast format understood by ocamlc/ocamlopt/ocamldep. Pros: - faster than parsing clear-text source file. diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 873adc1b22..fd3101613a 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -88,7 +88,7 @@ bootstrapped. The dependencies of a file FOO are in FOO.d . This enables partial recalculation of dependencies (only the dependencies of changed files are recomputed). -If you add a dependency to a Coq camlp4 extension (grammar.cma or +If you add a dependency to a Coq camlp5 extension (grammar.cma or q_constr.cmo), then see sections ".ml4 files" and "new files". Cleaning Targets @@ -127,7 +127,7 @@ of a grammar extension via a line of the form: The use of (*i camlp4use: ... i*) to mention uses of standard extension such as IFDEF has also been discontinued, the Makefile now -always calls camlp4 with pa_macros.cmo and a few others by default. +always calls camlp5 with pa_macros.cmo and a few others by default. For debugging a Coq grammar extension, it could be interesting to use the READABLE_ML4=1 option, otherwise the generated .ml are @@ -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/changes.md b/dev/doc/changes.md index aef62b0092..ab78b0956f 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -20,6 +20,14 @@ General deprecation removed. Please, make sure your plugin is warning-free in 8.7 before trying to port it over 8.8. +Proof engine + + Due to the introduction of `EConstr` in 8.7, it is not necessary to + track "goal evar normal form status" anymore, thus the type `'a + Proofview.Goal.t` loses its ghost argument. This may introduce some + minor incompatibilities at the typing level. Code-wise, things + should remain the same. + We removed the following functions: - `Universes.unsafe_constr_of_global`: use `Global.constr_of_global_in_context` @@ -41,6 +49,14 @@ We changed the type of the following functions: a functional way. The old style of passing `evar_map`s as references is not supported anymore. +Changes in the abstract syntax tree: + +- The practical totality of the AST has been nodified using + `CAst.t`. This means that all objects coming from parsing will be + indeed wrapped in a `CAst.t`. `Loc.located` is on its way to + deprecation. Some minor interfaces changes have resulted from + this. + We have changed the representation of the following types: - `Lib.object_prefix` is now a record instead of a nested tuple. diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index 2dbd132da7..b3d49b7e56 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -25,7 +25,7 @@ intf : grammar : - Camlp4 syntax extensions. The file grammar/grammar.cma is used + Camlp5 syntax extensions. The file grammar/grammar.cma is used to pre-process .ml4 files containing EXTEND constructions, either TACTIC EXTEND, ARGUMENTS EXTEND or VERNAC ... EXTEND. This grammar.cma incorporates many files from other directories diff --git a/dev/header b/dev/header deleted file mode 100644 index bf7bdc1699..0000000000 --- a/dev/header +++ /dev/null @@ -1,7 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) 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.ml b/dev/header.ml new file mode 100644 index 0000000000..7c3ee60040 --- /dev/null +++ b/dev/header.ml @@ -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.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/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 3cbccab44c..f3e60edea8 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -3,19 +3,19 @@ # Wrapper around ocamldebug for Coq # This file is to be launched via the generated script ocamldebug-coq, -# which will set the env variables $OCAMLDEBUG, $CAMLP4LIB, $COQTOP +# which will set the env variables $OCAMLDEBUG, $CAMLP5LIB, $COQTOP # Anyway, just in case someone tries to use this script directly, # here are some reasonable default values [ -z "$OCAMLDEBUG" ] && OCAMLDEBUG=ocamldebug -[ -z "$CAMLP4LIB" ] && CAMLP4LIB=+camlp5 +[ -z "$CAMLP5LIB" ] && CAMLP5LIB=+camlp5 [ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD [ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD` export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH exec $OCAMLDEBUG \ - -I $CAMLP4LIB -I +threads \ + -I $CAMLP5LIB -I +threads \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ diff --git a/dev/tools/anomaly-traces-parser.el b/dev/tools/anomaly-traces-parser.el deleted file mode 100644 index 68f54266f9..0000000000 --- a/dev/tools/anomaly-traces-parser.el +++ /dev/null @@ -1,28 +0,0 @@ -;; This Elisp snippet adds a regexp parser for the format of Anomaly -;; backtraces (coqc -bt ...), to the error parser of the Compilation -;; mode (C-c C-c: "Compile command: ..."). Once the -;; coq-change-error-alist-for-backtraces function has run, file -;; locations in traces are recognized and can be jumped from easily -;; from the *compilation* buffer. - -;; You can just copy everything below to your .emacs and this will be -;; enabled from any compilation command launched from an OCaml file. - -(defun coq-change-error-alist-for-backtraces () - "Hook to change the compilation-error-regexp-alist variable, to - search the coq backtraces for error locations" - (interactive) - (add-to-list - 'compilation-error-regexp-alist-alist - '(coq-backtrace - "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\ - lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\ - \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)" - 2 (3 . 4) (5 . 6))) - (add-to-list 'compilation-error-regexp-alist 'coq-backtrace)) - -;; this Anomaly parser should be available when one is hacking -;; on the *OCaml* code of Coq (adding bugs), so we enable it -;; through the OCaml mode hooks. -(add-hook 'caml-mode-hook 'coq-change-error-alist-for-backtraces) -(add-hook 'tuareg-mode-hook 'coq-change-error-alist-for-backtraces) diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index d7acf01f1d..e4359f7038 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -50,6 +50,15 @@ else fi +if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then + echo + read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r + echo + if [[ ! $REPLY =~ ^[Yy]$ ]]; then + exit 1 + fi +fi + if [[ "${OPTION}" == "--stop-before-merging" ]]; then exit 0 fi diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh index 9e4c8661dc..e244d9ab80 100755 --- a/dev/tools/check-eof-newline.sh +++ b/dev/tools/check-eof-newline.sh @@ -1,13 +1,40 @@ #!/usr/bin/env bash +# Usage: check-eof-newline.sh [--fix] FILES... +# Detect missing end of file newlines for FILES. +# Files are skipped if untracked by git and depending on gitattributes. +# With --fix, automatically append a newline. +# Exit status: +# Without --fix: 1 if any file had a missing newline, 0 otherwise. +# With --fix: 1 if any non writable file had a missing newline, 0 otherwise. + +FIX= +if [ "$1" = --fix ]; +then + FIX=1 + shift +fi + CODE=0 for f in "$@"; do if git ls-files --error-unmatch "$f" >/dev/null 2>&1 && \ git check-attr whitespace -- "$f" | grep -q -v -e 'unset$' -e 'unspecified$' && \ [ -n "$(tail -c 1 "$f")" ] then - echo "No newline at end of file $f!" - CODE=1 + if [ -n "$FIX" ]; + then + if [ -w "$f" ]; + then + echo >> "$f" + echo "Newline appended to file $f!" + else + echo "File $f is missing a newline and not writable!" + CODE=1 + fi + else + echo "No newline at end of file $f!" + CODE=1 + fi fi done diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el new file mode 100644 index 0000000000..62fdaec802 --- /dev/null +++ b/dev/tools/coqdev.el @@ -0,0 +1,107 @@ +;;; coqdev.el --- Emacs helpers for Coq development -*- lexical-binding:t -*- + +;; Copyright (C) 2018 The Coq Development Team + +;; Maintainer: coqdev@inria.fr + +;;; Commentary: + +;; Helpers to set compilation commands, proof general variables, etc +;; for Coq development + +;; You can disable individual features without editing this file by +;; using `remove-hook', for instance +;; (remove-hook 'hack-local-variables-hook #'coqdev-setup-compile-command) + +;;; Installation: + +;; To use this, with coqdev.el located at /path/to/coqdev.el, add the +;; following to your init: + +;; (add-to-list 'load-path "/path/to/coqdev/") +;; (require 'coqdev) + +;; If you load this file from a git repository, checking out an old +;; commit will make it disappear and cause errors for your Emacs +;; startup. To ignore those errors use (require 'coqdev nil t). If you +;; check out a malicious commit Emacs startup would allow it to run +;; arbitrary code, to avoid this you can copy coqdev.el to any +;; location and adjust the load path accordingly (of course if you run +;; ./configure to compile Coq it is already too late). + +;;; Code: + +(defun coqdev-default-directory () + "Return the Coq repository containing `default-directory'." + (let ((dir (locate-dominating-file default-directory "META.coq"))) + (when dir (expand-file-name dir)))) + +(defun coqdev-setup-compile-command () + "Setup `compile-command' for Coq development." + (let ((dir (coqdev-default-directory))) + ;; we add a space at the end to make it easy to add arguments (eg -j or target) + (when dir (setq-local compile-command (concat "make -C " (shell-quote-argument dir) " "))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-compile-command) + +(defvar camldebug-command-name) ; from camldebug.el (caml package) +(defvar ocamldebug-command-name) ; from ocamldebug.el (tuareg package) +(defun coqdev-setup-camldebug () + "Setup ocamldebug for Coq development. + +Specifically `camldebug-command-name' and `ocamldebug-command-name'." + (let ((dir (coqdev-default-directory))) + (when dir + (setq-local camldebug-command-name + (concat dir "dev/ocamldebug-coq")) + (setq-local ocamldebug-command-name + (concat dir "dev/ocamldebug-coq"))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-camldebug) + +(defun coqdev-setup-tags () + "Setup `tags-file-name' for Coq development." + (let ((dir (coqdev-default-directory))) + (when dir (setq-local tags-file-name (concat dir "TAGS"))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-tags) + +(defvar coq-prog-args) +(defvar coq-prog-name) + +;; Lets us detect whether there are file local variables +;; even though PG sets it with `setq' when there's a _Coqproject. +;; Also makes sense generally, so might make it into PG someday. +(make-variable-buffer-local 'coq-prog-args) +(setq-default coq-prog-args nil) + +(defun coqdev-setup-proofgeneral () + "Setup Proofgeneral variables for Coq development. + +Note that this function is executed before _Coqproject is read if it exists." + (let ((dir (coqdev-default-directory))) + (when dir + (unless coq-prog-args + (setq coq-prog-args + `("-coqlib" ,dir "-R" ,(concat dir "plugins") + "Coq" "-R" ,(concat dir "theories") + "Coq"))) + (setq-local coq-prog-name (concat dir "bin/coqtop"))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral) + +;; This Elisp snippet adds a regexp parser for the format of Anomaly +;; backtraces (coqc -bt ...), to the error parser of the Compilation +;; mode (C-c C-c: "Compile command: ..."). File locations in traces +;; are recognized and can be jumped from easily in the *compilation* +;; buffer. +(defvar compilation-error-regexp-alist-alist) +(defvar compilation-error-regexp-alist) +(with-eval-after-load 'compile + (add-to-list + 'compilation-error-regexp-alist-alist + '(coq-backtrace + "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\ + lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\ + \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)" + 2 (3 . 4) (5 . 6))) + (add-to-list 'compilation-error-regexp-alist 'coq-backtrace)) + +(provide 'coqdev) +;;; coqdev ends here diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit new file mode 100755 index 0000000000..c9cdee84ab --- /dev/null +++ b/dev/tools/pre-commit @@ -0,0 +1,73 @@ +#!/bin/sh + +# configure automatically sets up a wrapper at .git/hooks/pre-commit +# which calls this script (if it exists). + +set -e + +if ! git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh || + ! git diff-index --check --cached HEAD >/dev/null 2>&1 ; +then + 1>&2 echo "Auto fixing whitespace issues..." + + # We fix whitespace in the index and in the working tree + # separately to preserve non-added changes. + index=$(mktemp "git-fix-ws-index.XXXXX") + fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXX") + tree=$(mktemp "git-fix-ws-tree.XXXXX") + 1>&2 echo "Patches are saved in '$index', '$fixed_index' and '$tree'." + 1>&2 echo "If an error destroys your changes you can recover using them." + 1>&2 echo "(The files are cleaned up on success.)" + 1>&2 echo #newline + + git diff-index -p --cached HEAD > "$index" + git diff-index -p HEAD > "$tree" + + # reset work tree and index + # NB: untracked files which were not added are untouched + git apply --cached -R "$index" + git apply -R "$tree" + + # Fix index + # For end of file newlines we must go through the worktree + 1>&2 echo "Fixing staged changes..." + git apply --cached --whitespace=fix "$index" + git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself + git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix + git add -u + 1>&2 echo #newline + + # reset work tree + git diff-index -p --cached HEAD > "$fixed_index" + # If all changes were bad whitespace changes the patch is empty + # making git fail. Don't fail now: we fix the worktree first. + if [ -s "$fixed_index" ] + then + git apply -R "$fixed_index" + fi + + # Fix worktree + 1>&2 echo "Fixing unstaged changes..." + git apply --whitespace=fix "$tree" + git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix + 1>&2 echo #newline + + if ! [ -s "$fixed_index" ] + then + 1>&2 echo "No changes after fixing whitespace issues!" + exit 1 + fi + + # Check that we did fix whitespace + if ! git diff-index --check --cached HEAD; + then + 1>&2 echo "Auto-fixing whitespace failed: errors remain." + 1>&2 echo "This may fix itself if you try again." + 1>&2 echo "(Consider whether the number of errors decreases after each run.)" + exit 1 + fi + 1>&2 echo "Whitespace issues fixed!" + + # clean up temporary files + rm "$index" "$tree" "$fixed_index" +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index af38ce4b8c..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")" @@ -485,7 +491,7 @@ let in_current_context f c = let (evmap,sign) = Pfedit.get_current_context () in f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*) -(* We expand the result of preprocessing to be independent of camlp4 +(* We expand the result of preprocessing to be independent of camlp5 VERNAC COMMAND EXTEND PrintPureConstr | [ "PrintPureConstr" constr(c) ] -> [ in_current_context print_pure_constr c ] @@ -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() |