diff options
103 files changed, 1990 insertions, 233 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index b0e79fb1b2..2a641263e3 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -71,6 +71,8 @@ azure-pipelines.yml @coq/ci-maintainers /man/ @silene # Secondary maintainer @maximedenes +/doc/plugin_tutorial/ @ybertot + ########## Coqchk ########## /checker/ @ppedrot diff --git a/.gitignore b/.gitignore index 0411247abf..dfecfec837 100644 --- a/.gitignore +++ b/.gitignore @@ -150,6 +150,7 @@ kernel/byterun/coq_jumptbl.h kernel/copcodes.ml ide/index_urls.txt .lia.cache +.nia.cache # emacs save files *~ diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f131a97ba5..e981c592a2 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -151,7 +151,7 @@ after_script: - BIN=$(readlink -f ../_install_ci/bin)/ - LIB=$(readlink -f ../_install_ci/lib/coq)/ - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH" - - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" all + - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" COQFLAGS="${COQFLAGS}" all artifacts: name: "$CI_JOB_NAME.logs" when: on_failure @@ -245,6 +245,12 @@ build:base+async: COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" COQUSERFLAGS: "-async-proofs on" +build:quick: + <<: *build-template + variables: + COQ_EXTRA_CONF: "-native-compiler no" + QUICK: "1" + windows64: <<: *windows-template variables: @@ -427,6 +433,13 @@ test-suite:edge+trunk+dune: expire_in: 1 week allow_failure: true +test-suite:base+async: + <<: *test-suite-template + dependencies: + - build:base + variables: + COQFLAGS: "-async-proofs on" + validate:base: <<: *validate-template dependencies: @@ -454,6 +467,11 @@ validate:edge+flambda: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" +validate:quick: + <<: *validate-template + dependencies: + - build:quick + # Libraries are by convention the projects that depend on Coq # but not on its ML API @@ -485,7 +503,7 @@ library:ci-fiat-crypto-legacy: library:ci-flocq: <<: *ci-template -library:ci-formal-topology: +library:ci-corn: <<: *ci-template-flambda library:ci-geocoq: @@ -506,6 +524,9 @@ library:ci-sf: library:ci-unimath: <<: *ci-template-flambda +library:ci-verdi-raft: + <<: *ci-template-flambda + library:ci-vst: <<: *ci-template-flambda @@ -541,8 +562,12 @@ plugin:ci-mtac2: plugin:ci-paramcoq: <<: *ci-template -plugin:ci-plugin_tutorial: - <<: *ci-template +plugin:plugin-tutorial: + stage: test + dependencies: [] + script: + - ./configure -local -warn-error yes + - make -j "$NJOBS" plugin-tutorial plugin:ci-quickchick: <<: *ci-template-flambda @@ -10,6 +10,7 @@ ## either amend this file and commit it, or contact the coqdev list Abhishek Anand <abhishek.anand.iitg@gmail.com> Abhishek Anand (@brixpro-home) <abhishek.anand.iitg@gmail.com> +Léo Andrès <leo@ndrs.fr> zapashcanon <leo@ndrs.fr> Jim Apple <github.public@jbapple.com> jbapple <github.public@jbapple.com> Bruno Barras <bruno.barras@inria.fr> barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> Bruno Barras <bruno.barras@inria.fr> barras-local <barras-local@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -19,9 +20,11 @@ Yves Bertot <yves.bertot@inria.fr> Yves Bertot <bertot@inria.fr> Yves Bertot <yves.bertot@inria.fr> Yves Bertot <Yves.Bertot@inria.fr> Frédéric Besson <frederic.besson@inria.fr> fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> Siddharth Bhat <siddu.druid@gmail.com> Siddharth <siddu.druid@gmail.com> +Simon Boulier <simon.boulier@ens-rennes.fr> SimonBoulier <simon.boulier@ens-rennes.fr> Pierre Boutillier <pierre.boutillier@ens-lyon.org> pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre Boutillier <pierre.boutillier@ens-lyon.org> Pierre <pierre.boutillier@ens-lyon.org> Pierre Boutillier <pierre.boutillier@ens-lyon.org> Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> +Arthur Charguéraud <arthur@chargueraud.org> charguer <arthur@chargueraud.org> Xavier Clerc <xavier.clerc@inria.fr> xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> Xavier Clerc <xavier.clerc@inria.fr> xclerc <xavier.clerc@inria.fr> Pierre Corbineau <Pierre.Corbineau@NOSPAM@imag.fr> corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -32,6 +35,7 @@ Maxime Dénès <mail@maximedenes.fr> mdenes <mdenes@85f007b7-540 Maxime Dénès <mail@maximedenes.fr> Maxime Denes <maximedenes@gillespie.inria.fr> Olivier Desmettre <desmettr@gforge> desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> Damien Doligez <doligez@gforge> doligez <doligez@85f007b7-540e-0410-9357-904b9bb8a0f7> +İsmail Dönmez <ismail-s@users.noreply.github.com> Ismail <ismail-s@users.noreply.github.com> Andres Erbsen <andreser@mit.edu> Andres Erbsen <andres@kevix.co> Jim Fehrle <jfehrle@sbcglobal.net> Jim <jfehrle@sbcglobal.net> Jean-Christophe Filliâtre <Jean-Christophe.Filliatre@lri.fr> filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -63,11 +67,14 @@ Florent Kirchner <fkirchne@gforge> kirchner <kirchner@85f007b7-5 Johannes Kloos <jkloos@mpi-sws.org> jkloos <jkloos@mpi-sws.org> Matej Košík <matej.kosik@inria.fr> Matej Kosik <m4tej.kosik@gmail.com> Matej Košík <matej.kosik@inria.fr> Matej Kosik <matej.kosik@inria.fr> +Ambroise Lafont <chaster_killer@hotmail.fr> amblaf <you@example.com> +Ambroise Lafont <chaster_killer@hotmail.fr> Ambroise <chaster_killer@hotmail.fr> Vincent Laporte <Vincent.Laporte@fondation-inria.fr> Vincent Laporte <Vincent.Laporte@gmail.com> Marc Lasson <marc.lasson@gmail.com> mlasson <marc.lasson@gmail.com> William Lawvere <mundungus.corleone@gmail.com> william-lawvere <mundungus.corleone@gmail.com> Pierre Letouzey <pierre.letouzey@inria.fr> letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre Letouzey <pierre.letouzey@inria.fr> letouzey <pierre.letouzey@inria.fr> +Xia Li-yao <lysxia@gmail.com> Lysxia <lysxia@gmail.com> Assia Mahboubi <assia.mahboubi@inria.fr> amahboub <amahboub@85f007b7-540e-0410-9357-904b9bb8a0f7> Evgeny Makarov <emakarov@gforge> emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> Gregory Malecha <gmalecha@eecs.harvard.edu> Gregory Malecha <gmalecha@cs.harvard.edu> @@ -88,6 +95,7 @@ Russell O'Connor <roconnor@blockstream.io> roconnor-blockstream <roconno Christine Paulin <cpaulin@gforge> cpaulin <cpaulin@85f007b7-540e-0410-9357-904b9bb8a0f7> Christine Paulin <cpaulin@gforge> mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> +Frederic Peschanski <frederic.peschanski@lip6.fr> fredokun <frederic.peschanski@lip6.fr> Clément Pit-Claudel <clement.pitclaudel@live.com> Clément Pit--Claudel <clement.pitclaudel@live.com> Loïc Pottier <pottier@gforge> pottier <pottier@85f007b7-540e-0410-9357-904b9bb8a0f7> Matthias Puech <puech@gforge> puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -98,6 +106,7 @@ Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel De Rauglaudre <ddr@g Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7> Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> Regis-Gianas <yrg@pps.univ-paris-diderot.fr> Clément Renard <clrenard@gforge> clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> +Matthew Ryan <mr_1993@hotmail.co.uk> mrmr1993 <mr_1993@hotmail.co.uk> Claudio Sacerdoti Coen <sacerdot@gforge> sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> Kazuhiko Sakaguchi <pi8027@gmail.com> Kazuhiko Sakaguchi <sakaguchi@coins.tsukuba.ac.jp> Vincent Siles <vsiles@gforge> vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -108,6 +117,7 @@ Matthieu Sozeau <mattam@mattam.org> Matthieu Sozeau <matthieu.soz Matthieu Sozeau <mattam@mattam.org> Matthieu Sozeau <mattam@eduroam-prg-sg-1-46-137.net.univ-paris-diderot.fr> Arnaud Spiwack <arnaud@spiwack.net> aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> Paul Steckler <steck@stecksoft.com> Paul Steckler <psteck@mit.edu> +Frank Steffahn <fdsteffahn@gmail.com> staffehn <fdsteffahn@gmail.com> Enrico Tassi <Enrico.Tassi@inria.fr> gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> Enrico Tassi <Enrico.Tassi@inria.fr> Enrico Tassi <enrico.tassi@inria.fr> Enrico Tassi <Enrico.Tassi@inria.fr> Enrico Tassi <gares@fettunta.org> @@ -123,5 +133,8 @@ Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> Théo Zimmermann <theo. # Anonymous accounts anonymous < > coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> -anonymous < > (no author) <(no author)@85f007b7-540e-0410-9357-904b9bb8a0f7> -anonymous < > serpyc <serpyc@85f007b7-540e-0410-9357-904b9bb8a0f7> + +# Bot accounts + +cvs2svn < > (no author) <(no author)@85f007b7-540e-0410-9357-904b9bb8a0f7> +serpyc-bot < > serpyc <serpyc@85f007b7-540e-0410-9357-904b9bb8a0f7> diff --git a/CHANGES.md b/CHANGES.md index 6789bc038e..ae67eb5d1b 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -93,6 +93,9 @@ Vernacular commands - The naming scheme for anonymous binders in a `Theorem` has changed to avoid conflicts with explicitly named binders. +- Computation of implicit arguments now properly handles local definitions in the + binders for an `Instance`. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: @@ -61,7 +61,8 @@ FIND_SKIP_DIRS:='(' \ -name 'user-contrib' -o \ -name 'test-suite' -o \ -name '.opamcache' -o \ - -name '.coq-native' \ + -name '.coq-native' -o \ + -name 'plugin_tutorial' \ ')' -prune -o define find @@ -191,7 +192,7 @@ META.coq: META.coq.in # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean plugin-tutorialclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean clean: objclean cruftclean depclean docclean camldevfilesclean gramlibclean @@ -237,7 +238,7 @@ docclean: rm -f doc/coq.tex rm -rf doc/sphinx/_build -archclean: clean-ide optclean voclean +archclean: clean-ide optclean voclean plugin-tutorialclean rm -rf _build rm -f $(ALLSTDLIB).* @@ -268,7 +269,7 @@ cleanconfig: distclean: clean cleanconfig cacheclean timingclean voclean: - find theories plugins test-suite \( -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" \ + find theories plugins test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.glob' -o -name "*.cmxs" \ -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} + find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} + @@ -278,6 +279,9 @@ timingclean: -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \ -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} + +plugin-tutorialclean: + +$(MAKE) -C $(PLUGINTUTO) clean + # Ensure that every compiled file around has a known source file. # This should help preventing weird compilation failures caused by leftover # compiled files after deleting or moving some source files. diff --git a/Makefile.build b/Makefile.build index 34d7ce42f7..e683a6bda8 100644 --- a/Makefile.build +++ b/Makefile.build @@ -57,6 +57,9 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line BEFORE ?= AFTER ?= +# Number of parallel jobs for -schedule-vio2vo +NJOBS ?= 2 + ########################################################################### # Default starting rule ########################################################################### @@ -543,7 +546,7 @@ $(CSDPCERTBYTE): $(CSDPCERTCMO) VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m -validate: $(CHICKEN) | $(ALLVO) +validate: $(CHICKEN) | $(ALLVO:.$(VO)=.vo) $(SHOW)'COQCHK <theories & plugins>' $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS) @@ -779,13 +782,19 @@ $(PLUGMLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter plugins/%, $(MLLIBFILES) $( # since they are all mentioned in at least one Declare ML Module in some .v coqlib: theories plugins +ifdef QUICK + $(SHOW)'COQC -schedule-vio2vo $(NJOBS) theories/**.vio plugins/**.vio' + $(HIDE)$(BOOTCOQC:-compile=-schedule-vio2vo) $(NJOBS) \ + $(THEORIESVO) $(PLUGINSVO) +endif + coqlib.timing.diff: theories.timing.diff plugins.timing.diff theories: $(THEORIESVO) plugins: $(PLUGINSVO) -theories.timing.diff: $(THEORIESVO:.vo=.v.timing.diff) -plugins.timing.diff: $(PLUGINSVO:.vo=.v.timing.diff) +theories.timing.diff: $(THEORIESVO:.$(VO)=.v.timing.diff) +plugins.timing.diff: $(PLUGINSVO:.$(VO)=.v.timing.diff) .PHONY: coqlib theories plugins coqlib.timing.diff theories.timing.diff plugins.timing.diff @@ -802,6 +811,10 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) $(HIDE)rm -f theories/Init/$*.glob $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA) +theories/Init/%.vio: theories/Init/%.v $(VO_TOOLS_DEP) + $(SHOW)'COQC -quick -noinit $<' + $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq -quick -noglob + # The general rule for building .vo files : %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) @@ -814,6 +827,10 @@ ifdef VALIDATE || ( RV=$$?; rm -f "$@"; exit $${RV} ) endif +%.vio: %.v theories/Init/Prelude.vio $(VO_TOOLS_DEP) + $(SHOW)'COQC -quick $<' + $(HIDE)$(BOOTCOQC) $< -quick -noglob + %.v.timing.diff: %.v.before-timing %.v.after-timing $(SHOW)PYTHON TIMING-DIFF $< $(HIDE)$(MAKE) --no-print-directory print-pretty-single-time-diff BEFORE=$*.v.before-timing AFTER=$*.v.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" diff --git a/Makefile.ci b/Makefile.ci index 2df6a792b6..b8bff98f5f 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -27,7 +27,6 @@ CI_TARGETS= \ ci-fiat-crypto-legacy \ ci-fiat-parsers \ ci-flocq \ - ci-formal-topology \ ci-geocoq \ ci-coqhammer \ ci-hott \ @@ -37,13 +36,13 @@ CI_TARGETS= \ ci-math-comp \ ci-mtac2 \ ci-paramcoq \ - ci-plugin_tutorial \ ci-quickchick \ ci-relation-algebra \ ci-sf \ ci-simple-io \ ci-tlc \ ci-unimath \ + ci-verdi-raft \ ci-vst .PHONY: ci-all $(CI_TARGETS) @@ -63,8 +62,6 @@ ci-corn: ci-math-classes ci-simple-io: ci-ext-lib ci-quickchick: ci-ext-lib ci-simple-io -ci-formal-topology: ci-corn - # Generic rule, we use make to ease CI integration $(CI_TARGETS): ci-%: +./dev/ci/ci-wrapper.sh $* diff --git a/Makefile.common b/Makefile.common index 9f7ed9d46e..2dced04967 100644 --- a/Makefile.common +++ b/Makefile.common @@ -168,6 +168,8 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx) ALLSTDLIB := test-suite/misc/universes/all_stdlib +PLUGINTUTO := doc/plugin_tutorial + # For emacs: # Local Variables: # mode: makefile diff --git a/Makefile.dev b/Makefile.dev index 9659f602d7..13b85dfad4 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -63,7 +63,7 @@ revision: coqlight: theories-light tools coqbinaries -states: theories/Init/Prelude.vo +states: theories/Init/Prelude.$(VO) miniopt: $(COQTOPEXE) pluginsopt minibyte: $(COQTOPBYTE) pluginsbyte diff --git a/Makefile.doc b/Makefile.doc index 9e6ec4955a..7ac710b8c9 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -89,6 +89,10 @@ stdlib: \ full-stdlib: \ doc/stdlib/html/index.html doc/stdlib/FullLibrary.ps doc/stdlib/FullLibrary.pdf +.PHONY: plugin-tutorial +plugin-tutorial: states tools + +$(MAKE) COQBIN=$(PWD)/bin/ -C $(PLUGINTUTO) + ###################################################################### ### Implicit rules ###################################################################### @@ -137,7 +141,7 @@ else doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO) endif $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ - -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ + -R theories Coq $(THEORIESLIGHTVO:.$(VO)=.v) >> $@ doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex (cd doc/stdlib;\ diff --git a/Makefile.ide b/Makefile.ide index cae77ee348..23ce83d263 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -70,7 +70,7 @@ SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-2.0)/share .PHONY: ide-toploop ide-byteloop ide-optloop # target to build CoqIde (native version) and the stuff needed to lauch it -coqide: coqide-files coqide-opt theories/Init/Prelude.vo +coqide: coqide-files coqide-opt theories/Init/Prelude.$(VO) # target to build CoqIde (in native and byte versions), and no more # NB: this target is used in the opam package coq-coqide diff --git a/Makefile.vofiles b/Makefile.vofiles index d0ae317335..d5217ef4b7 100644 --- a/Makefile.vofiles +++ b/Makefile.vofiles @@ -2,14 +2,20 @@ # This file calls [find] and as such is not suitable for inclusion in # the test suite Makefile, unlike Makefile.common. +ifdef QUICK +VO=vio +else +VO=vo +endif + ########################################################################### # vo files ########################################################################### -THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v")) -PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v")) +THEORIESVO := $(patsubst %.v,%.$(VO),$(shell find theories -type f -name "*.v")) +PLUGINSVO := $(patsubst %.v,%.$(VO),$(shell find plugins -type f -name "*.v")) ALLVO := $(THEORIESVO) $(PLUGINSVO) -VFILES := $(ALLVO:.vo=.v) +VFILES := $(ALLVO:.$(VO)=.v) ## More specific targets @@ -20,22 +26,27 @@ THEORIESLIGHTVO:= \ # remove .vo, replace theories and plugins by Coq, and replace slashes by dots vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=)))) -ALLMODS:=$(call vo_to_mod,$(ALLVO)) +ALLMODS:=$(call vo_to_mod,$(ALLVO:.$(VO)=.vo)) # Converting a stdlib filename into native compiler filenames # Used for install targets -vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*))))) +vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.cm*))))) -vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o))))) +vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o))))) + +ifdef QUICK +GLOBFILES:= +else +GLOBFILES:=$(ALLVO:.$(VO)=.glob) +endif -GLOBFILES:=$(ALLVO:.vo=.glob) ifdef NATIVECOMPUTE NATIVEFILES := $(call vo_to_cm,$(ALLVO)) $(call vo_to_obj,$(ALLVO)) else NATIVEFILES := endif -LIBFILES:=$(ALLVO) $(NATIVEFILES) $(VFILES) $(GLOBFILES) +LIBFILES:=$(ALLVO:.$(VO)=.vo) $(NATIVEFILES) $(VFILES) $(GLOBFILES) # For emacs: # Local Variables: @@ -1,19 +1,68 @@ # Coq -[](https://gitlab.com/coq/coq/commits/master) -[](https://travis-ci.org/coq/coq/builds) -[](https://ci.appveyor.com/project/coq/coq/branch/master) -[](https://gitter.im/coq/coq) -[](https://doi.org/10.5281/zenodo.1003420) +[![GitLab][gitlab-badge]][gitlab-link] +[![Azure Pipelines][azure-badge]][azure-link] +[![Travis][travis-badge]][travis-link] +[![Appveyor][appveyor-badge]][appveyor-link] +[![Gitter][gitter-badge]][gitter-link] +[![DOI][doi-badge]][doi-link] + +[gitlab-badge]: https://gitlab.com/coq/coq/badges/master/pipeline.svg +[gitlab-link]: https://gitlab.com/coq/coq/commits/master + +[azure-badge]: https://dev.azure.com/coq/coq/_apis/build/status/coq.coq?branchName=master +[azure-link]: https://dev.azure.com/coq/coq/_build/latest?definitionId=1?branchName=master + +[travis-badge]: https://travis-ci.org/coq/coq.svg?branch=master +[travis-link]: https://travis-ci.org/coq/coq/builds + +[appveyor-badge]: https://ci.appveyor.com/api/projects/status/eln43k05pa2vm908/branch/master?svg=true +[appveyor-link]: https://ci.appveyor.com/project/coq/coq/branch/master + +[gitter-badge]: https://badges.gitter.im/coq/coq.svg +[gitter-link]: https://gitter.im/coq/coq + +[doi-badge]: https://zenodo.org/badge/DOI/10.5281/zenodo.1003420.svg +[doi-link]: https://doi.org/10.5281/zenodo.1003420 Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. ## Installation -Download the pre-built packages of the [latest release](https://github.com/coq/coq/releases/latest) for Windows and MacOS; -read the [help page](https://coq.inria.fr/opam/www/using.html) on how to install Coq with OPAM; -or refer to the [`INSTALL` file](INSTALL) for the procedure to install from source. + +[![latest packaged version(s)][repology-badge]][repology-link] + +[![Arch package][arch-badge]][arch-link] +[![Chocolatey package][chocolatey-badge]][chocolatey-link] +[![Homebrew package][homebrew-badge]][homebrew-link] +[![MacPorts package][macports-badge]][macports-link] +[![nixpkgs unstable package][nixpkgs-badge]][nixpkgs-link] + +[repology-badge]: https://repology.org/badge/latest-versions/coq.svg +[repology-link]: https://repology.org/metapackage/coq/versions + +[arch-badge]: https://repology.org/badge/version-for-repo/arch/coq.svg +[arch-link]: https://www.archlinux.org/packages/community/x86_64/coq/ + +[chocolatey-badge]: https://repology.org/badge/version-for-repo/chocolatey/coq.svg +[chocolatey-link]: https://chocolatey.org/packages/Coq + +[homebrew-badge]: https://repology.org/badge/version-for-repo/homebrew/coq.svg +[homebrew-link]: https://formulae.brew.sh/formula/coq + +[macports-badge]: https://repology.org/badge/version-for-repo/macports/coq.svg +[macports-link]: https://www.macports.org/ports.php?by=name&substr=coq + +[nixpkgs-badge]: https://repology.org/badge/version-for-repo/nix_unstable/coq.svg +[nixpkgs-link]: https://nixos.org/nixos/packages.html#coq + +Download the pre-built packages of the [latest release][] for Windows and macOS; +read the [help page][opam-using] on how to install Coq with OPAM; +or refer to the [`INSTALL`](INSTALL) file for the procedure to install from source. + +[latest release]: https://github.com/coq/coq/releases/latest +[opam-using]: https://coq.inria.fr/opam/www/using.html ## Documentation diff --git a/checker/check.ml b/checker/check.ml index 30437e8bd0..b2930d9535 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -329,7 +329,7 @@ let intern_from_file (dir, f) = user_err ~hdr:"intern_from_file" (str "The file "++str f++str " contains unfinished tasks"); if opaque_csts <> None then begin - chk_pp (str " (was a vio file) "); + Flags.if_verbose chk_pp (str " (was a vio file) "); Option.iter (fun (_,_,b) -> if not b then user_err ~hdr:"intern_from_file" (str "The file "++str f++str " is still a .vio")) diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index b202635714..07a13b8204 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -691,7 +691,7 @@ function installer_addon_end { # ------------------------------------------------------------------------------ function coq_set_timeouts_1000 { - find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/' + find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/g' } ###################### MODULE BUILD FUNCTIONS ##################### @@ -701,7 +701,7 @@ function coq_set_timeouts_1000 { function make_sed { if build_prep https://ftp.gnu.org/gnu/sed/ sed-4.2.2 tar.gz ; then logn configure ./configure - log1 make + log1 make $MAKE_OPT log2 make install log2 make clean build_post @@ -1107,7 +1107,7 @@ function make_ocamlbuild { make_ocaml if build_prep https://github.com/ocaml/ocamlbuild/archive 0.12.0 tar.gz 1 ocamlbuild-0.12.0; then log2 make configure OCAML_NATIVE=true OCAMLBUILD_PREFIX=$PREFIXOCAML OCAMLBUILD_BINDIR=$PREFIXOCAML/bin OCAMLBUILD_LIBDIR=$PREFIXOCAML/lib - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1634,7 +1634,7 @@ function make_addon_bignums { installer_addon_section bignums "Bignums" "Coq library for fast arbitrary size numbers" "" # To make command lines shorter :-( echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local - log1 make all + log1 make $MAKE_OPT all log2 make install build_post fi @@ -1650,7 +1650,7 @@ function make_addon_equations { # Note: PATH is automatically saved/restored by build_prep / build_post PATH=$COQBIN:$PATH logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1696,7 +1696,7 @@ function make_addon_ltac2 { installer_addon_dependency ltac2 if build_prep_overlay ltac2; then installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactic language" "" - log1 make all + log1 make $MAKE_OPT all log2 make install build_post fi @@ -1709,7 +1709,7 @@ function make_addon_unicoq { if build_prep_overlay unicoq; then installer_addon_section unicoq "Unicoq" "Coq plugin for an enhanced unification algorithm" "" log1 coq_makefile -f Make -o Makefile - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1724,7 +1724,7 @@ function make_addon_mtac2 { if build_prep_overlay mtac2; then installer_addon_section mtac2 "Mtac-2" "Coq plugin for a typed tactic language for Coq." "" log1 coq_makefile -f _CoqProject -o Makefile - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1766,7 +1766,7 @@ function make_addon_menhirlib { echo -R . MenhirLib > _CoqProject ls -1 *.v >> _CoqProject log1 coq_makefile -f _CoqProject -o Makefile.coq - log1 make -f Makefile.coq all + log1 make -f Makefile.coq $MAKE_OPT all logn make-install make -f Makefile.coq install build_post fi @@ -1779,10 +1779,10 @@ function make_addon_compcert { make_menhir make_addon_menhirlib installer_addon_dependency_end - if build_prep_overlay CompCert; then + if build_prep_overlay compcert; then installer_addon_section compcert "CompCert" "ATTENTION: THIS IS NOT OPEN SOURCE! CompCert verified C compiler and Clightgen (required for using VST for your own code)" "off" logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin - log1 make + log1 make $MAKE_OPT log2 make install logn install-license-1 install -D -T "LICENSE" "$PREFIXCOQ/lib/coq/user-contrib/compcert/LICENSE" logn install-license-2 install -D -T "LICENSE" "$PREFIXCOQ/lib/compcert/LICENSE" @@ -1807,8 +1807,8 @@ function install_addon_vst { install_glob "progs" '*.v' "$VSTDEST/progs/" install_glob "progs" '*.c' "$VSTDEST/progs/" install_glob "progs" '*.h' "$VSTDEST/progs/" - install_glob "veric" '*.v' "$VSTDEST/msl/" - install_glob "veric" '*.vo' "$VSTDEST/msl/" + install_glob "veric" '*.v' "$VSTDEST/veric/" + install_glob "veric" '*.vo' "$VSTDEST/veric/" # Install VST documentation files install_glob "." 'LICENSE' "$VSTDEST" @@ -1821,12 +1821,20 @@ function install_addon_vst { install_glob "." '_CoqProject-export' "$VSTDEST/progs" } +function vst_patch_compcert_refs { + find . -type f -name '*.v' -print0 | xargs -0 sed -E -i \ + -e 's/(Require\s+(Import\s+|Export\s+)*)compcert\./\1VST.compcert./g' \ + -e 's/From compcert Require/From VST.compcert Require/g' +} + function make_addon_vst { installer_addon_dependency vst - if build_prep_overlay VST; then + if build_prep_overlay vst; then installer_addon_section vst "VST" "ATTENTION: SOME INCLUDED COMPCERT PARTS ARE NOT OPEN SOURCE! Verified Software Toolchain for verifying C code" "off" - log1 coq_set_timeouts_1000 - log1 make IGNORECOQVERSION=true $MAKE_OPT + # log1 coq_set_timeouts_1000 + log1 vst_patch_compcert_refs + # The usage of the shell variable ARCH in VST collides with the usage in this shellscript + logn make env -u ARCH make IGNORECOQVERSION=true $MAKE_OPT log1 install_addon_vst build_post fi @@ -1851,9 +1859,9 @@ function make_addon_coquelicot { function make_addon_aactactics { installer_addon_dependency aac - if build_prep_overlay aactactics; then + if build_prep_overlay aac_tactics; then installer_addon_section aac "AAC" "Coq plugin for extensible associative and commutative rewriting" "" - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1894,7 +1902,7 @@ function make_addon_quickchick { installer_addon_dependency_end if build_prep_overlay quickchick; then installer_addon_section quickchick "QuickChick" "Coq plugin for randomized testing and counter example search" "" - log1 make + log1 make $MAKE_OPT log2 make install build_post fi diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch new file mode 100755 index 0000000000..2c8c46373f --- /dev/null +++ b/dev/build/windows/patches_coq/VST.patch @@ -0,0 +1,15 @@ +diff --git a/Makefile b/Makefile +index 4a119042..fdfac13e 100755 +--- a/Makefile ++++ b/Makefile +@@ -76,8 +76,8 @@ endif + + COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight $(BACKEND) + +-COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) compcert.$(d)) +-EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) compcert.$(d)) ++COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) VST.compcert.$(d)) ++EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) VST.compcert.$(d)) + + # for SSReflect + ifdef MATHCOMP diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index e0f4f50fa9..8dee465cf4 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -150,11 +150,11 @@ : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## -# formal-topology +# fiat_crypto_legacy ######################################################################## -: "${formal_topology_CI_REF:=ci}" -: "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}" -: "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}" +: "${fiat_crypto_legacy_CI_REF:=sp2019latest}" +: "${fiat_crypto_legacy_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" +: "${fiat_crypto_legacy_CI_ARCHIVEURL:=${fiat_crypto_legacy_CI_GITURL}/archive}" ######################################################################## # coq_dpdgraph @@ -240,13 +240,6 @@ : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" ######################################################################## -# plugin_tutorial -######################################################################## -: "${plugin_tutorial_CI_REF:=master}" -: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}" -: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}" - -######################################################################## # menhirlib ######################################################################## : "${menhirlib_CI_REF:=master}" @@ -273,3 +266,26 @@ : "${relation_algebra_CI_REF:=master}" : "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}" : "${relation_algebra_CI_ARCHIVEURL:=${relation_algebra_CI_GITURL}/archive}" + +######################################################################## +# StructTact + InfSeqExt + Cheerios + Verdi + Verdi Raft +######################################################################## +: "${struct_tact_CI_REF:=master}" +: "${struct_tact_CI_GITURL:=https://github.com/uwplse/StructTact}" +: "${struct_tact_CI_ARCHIVEURL:=${struct_tact_CI_GITURL}/archive}" + +: "${inf_seq_ext_CI_REF:=master}" +: "${inf_seq_ext_CI_GITURL:=https://github.com/DistributedComponents/InfSeqExt}" +: "${inf_seq_ext_CI_ARCHIVEURL:=${inf_seq_ext_CI_GITURL}/archive}" + +: "${cheerios_CI_REF:=master}" +: "${cheerios_CI_GITURL:=https://github.com/uwplse/cheerios}" +: "${cheerios_CI_ARCHIVEURL:=${cheerios_CI_GITURL}/archive}" + +: "${verdi_CI_REF:=master}" +: "${verdi_CI_GITURL:=https://github.com/uwplse/verdi}" +: "${verdi_CI_ARCHIVEURL:=${verdi_CI_GITURL}/archive}" + +: "${verdi_raft_CI_REF:=master}" +: "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}" +: "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}" diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh index 6bf3138346..2af4b58201 100755 --- a/dev/ci/ci-fiat-crypto-legacy.sh +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -4,11 +4,11 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" FORCE_GIT=1 -git_download fiat_crypto +git_download fiat_crypto_legacy fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display" fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display" -( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ +( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \ ./etc/ci/remove_autogenerated.sh && \ make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 7e8013be9b..bba17314f7 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -10,5 +10,9 @@ git_download fiat_crypto # building the executables. # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 +fiat_crypto_CI_TARGETS1="c-files printlite lite" +fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem" + ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ - ulimit -s 32768 && make new-pipeline c-files ) + ulimit -s 32768 && \ + make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} ) diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh deleted file mode 100755 index 8be5a06ed2..0000000000 --- a/dev/ci/ci-formal-topology.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download formal_topology - -( cd "${CI_BUILD_DIR}/formal_topology" && make ) diff --git a/dev/ci/ci-plugin_tutorial.sh b/dev/ci/ci-plugin_tutorial.sh deleted file mode 100755 index 6c26a71a21..0000000000 --- a/dev/ci/ci-plugin_tutorial.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download plugin_tutorial - -( cd "${CI_BUILD_DIR}/plugin_tutorial" && \ - pushd tuto0 && make && popd && \ - pushd tuto1 && make && popd && \ - pushd tuto2 && make && popd && \ - pushd tuto3 && make && popd ) diff --git a/dev/ci/ci-verdi-raft.sh b/dev/ci/ci-verdi-raft.sh new file mode 100755 index 0000000000..3bcd52c464 --- /dev/null +++ b/dev/ci/ci-verdi-raft.sh @@ -0,0 +1,24 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download struct_tact + +( cd "${CI_BUILD_DIR}/struct_tact" && ./configure && make && make install ) + +git_download inf_seq_ext + +( cd "${CI_BUILD_DIR}/inf_seq_ext" && ./configure && make && make install ) + +git_download cheerios + +( cd "${CI_BUILD_DIR}/cheerios" && ./configure && make && make install ) + +git_download verdi + +( cd "${CI_BUILD_DIR}/verdi" && ./configure && make && make install ) + +git_download verdi_raft + +( cd "${CI_BUILD_DIR}/verdi_raft" && ./configure && make ) diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 386a3de204..2a42a6b58e 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -49,10 +49,9 @@ IF "%WINDOWS%" == "enabled_all_addons" ( -addon=compcert ^
-addon=extlib ^
-addon=quickchick ^
- -addon=coquelicot
- REM addons with build issues
- REM -addon=vst ^
- REM -addon=aactactics ^
+ -addon=coquelicot ^
+ -addon=vst ^
+ -addon=aactactics
) ELSE (
SET "EXTRA_ADDONS= "
)
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 5fd8a3b7d9..a27dacc5a7 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -198,8 +198,26 @@ if [ -z "$(git config user.signingkey)" ]; then warning "gpg will guess a key out of your git config user.* data" fi +# Generate commit message + +info "Fetching review data" +reviews=$(curl -s "$API/pulls/$PR/reviews") +msg="Merge PR #$PR: $TITLE" + +has_state() { + [ "$(jq -rc 'map(select(.user.login == "'"$1"'") | .state) | any(. == "'"$2"'")' <<< "$reviews")" = true ] +} + +for reviewer in $(jq -rc 'map(.user.login) | unique | join(" ")' <<< "$reviews" ); do + if has_state "$reviewer" APPROVED; then + msg=$(printf '%s\n' "$msg" | git interpret-trailers --trailer Reviewed-by="$reviewer") + elif has_state "$reviewer" COMMENTED; then + msg=$(printf '%s\n' "$msg" | git interpret-trailers --trailer Ack-by="$reviewer") + fi +done + info "merging" -git merge -v -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $TITLE" -e +git merge -v -S --no-ff FETCH_HEAD -m "$msg" -e # TODO: improve this check if ! git diff --quiet --diff-filter=A "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci/user-overlays; then diff --git a/doc/plugin_tutorial/.gitignore b/doc/plugin_tutorial/.gitignore new file mode 100644 index 0000000000..3e4978fac4 --- /dev/null +++ b/doc/plugin_tutorial/.gitignore @@ -0,0 +1,13 @@ +*.ml*.d +*.cm[ixt]* +Makefile.coq* +*~ +*.[ao] +.coqdeps.d +*.vo +*.glob +*.aux +*/*/.merlin + +# by convention g_foo.ml is generated +g_*.ml diff --git a/doc/plugin_tutorial/.travis.yml b/doc/plugin_tutorial/.travis.yml new file mode 100644 index 0000000000..556e0ac45a --- /dev/null +++ b/doc/plugin_tutorial/.travis.yml @@ -0,0 +1,38 @@ +dist: trusty +sudo: required +language: generic + +services: + - docker + +env: + global: + - NJOBS="2" + - CONTRIB_NAME="plugin_tutorials" + matrix: + - COQ_IMAGE="coqorg/coq:dev" + +install: | + # Prepare the COQ container + docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/$CONTRIB_NAME -w /home/coq/$CONTRIB_NAME ${COQ_IMAGE} + docker exec COQ /bin/bash --login -c " + # This bash script is double-quoted to interpolate Travis CI env vars: + echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\" + export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' + set -ex # -e = exit on failure; -x = trace for debug + opam list + " +script: +- echo -e "${ANSI_YELLOW}Building $CONTRIB_NAME...${ANSI_RESET}" && echo -en 'travis_fold:start:testbuild\\r' +- | + docker exec COQ /bin/bash --login -c " + export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' + set -ex + sudo chown -R coq:coq /home/coq/$CONTRIB_NAME + ( cd tuto0 && make ) + ( cd tuto1 && make ) + ( cd tuto2 && make ) + ( cd tuto3 && make ) + " +- docker stop COQ # optional +- echo -en 'travis_fold:end:testbuild\\r' diff --git a/doc/plugin_tutorial/LICENSE b/doc/plugin_tutorial/LICENSE new file mode 100644 index 0000000000..cf1ab25da0 --- /dev/null +++ b/doc/plugin_tutorial/LICENSE @@ -0,0 +1,24 @@ +This is free and unencumbered software released into the public domain. + +Anyone is free to copy, modify, publish, use, compile, sell, or +distribute this software, either in source code form or as a compiled +binary, for any purpose, commercial or non-commercial, and by any +means. + +In jurisdictions that recognize copyright laws, the author or authors +of this software dedicate any and all copyright interest in the +software to the public domain. We make this dedication for the benefit +of the public at large and to the detriment of our heirs and +successors. We intend this dedication to be an overt act of +relinquishment in perpetuity of all present and future rights to this +software under copyright law. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR +OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, +ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR +OTHER DEALINGS IN THE SOFTWARE. + +For more information, please refer to <http://unlicense.org> diff --git a/doc/plugin_tutorial/Makefile b/doc/plugin_tutorial/Makefile new file mode 100644 index 0000000000..7f1833fadd --- /dev/null +++ b/doc/plugin_tutorial/Makefile @@ -0,0 +1,21 @@ + +TUTOS:= \ + tuto0 \ + tuto1 \ + tuto2 \ + tuto3 + +all: $(TUTOS) + +.PHONY: $(TUTOS) all + +$(TUTOS): %: + +$(MAKE) -C $@ + +CLEANS:=$(addsuffix -clean, $(TUTOS)) +.PHONY: clean $(CLEANS) + +clean: $(CLEANS) + +%-clean: + +$(MAKE) -C $* clean diff --git a/doc/plugin_tutorial/README.md b/doc/plugin_tutorial/README.md new file mode 100644 index 0000000000..f82edb2352 --- /dev/null +++ b/doc/plugin_tutorial/README.md @@ -0,0 +1,86 @@ +How to write plugins in Coq +=========================== + # Working environment : merlin, tuareg (open question) + + ## OCaml & related tools + + These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html) + +```shell +opam init --root=$PWD/CIW2018 --compiler=4.06.0 -j2 +eval `opam config env --root=$PWD/CIW2018` +opam install camlp5 ocamlfind num # Coq's dependencies +opam install lablgtk # Coqide's dependencies (optional) +opam install merlin # prints instructions for vim and emacs +``` + + ## Coq + +```shell +git clone git@github.com:coq/coq.git +cd coq +./configure -profile devel +make -j2 +cd .. +export PATH=$PWD/coq/bin:$PATH +``` + + ## This tutorial + +```shell +git clone git@github.com:ybertot/plugin_tutorials.git +cd plugin_tutorials/tuto0 +make .merlin # run before opening .ml files in your editor +make # build +``` + + + + # tuto0 : basics of project organization + package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject` + - Example of syntax to add a new toplevel command + - Example of function call to print a simple message + - Example of syntax to add a simple tactic + (that does nothing and prints a message) + - To use it: + +```bash + cd tuto0; make + coqtop -I src -R theories Tuto0 +``` + + In the Coq session type: +```coq + Require Import Tuto0.Loader. HelloWorld. +``` + + # tuto1 : Ocaml to Coq communication + Explore the memory of Coq, modify it + - Commands that take arguments: strings, symbols, expressions of the calculus of constructions + - Commands that interact with type-checking in Coq + - A command that adds a new definition or theorem + - A command that uses a name and exploits the existing definitions + or theorems + - A command that exploits an existing ongoing proof + - A command that defines a new tactic + + Compilation and loading must be performed as for `tuto0`. + + # tuto2 : Ocaml to Coq communication + A more step by step introduction to writing commands + - Explanation of the syntax of entries + - Adding a new type to and parsing to the available choices + - Handling commands that store information in user-chosen registers and tables + + Compilation and loading must be performed as for `tuto1`. + + # tuto3 : manipulating terms of the calculus of constructions + Manipulating terms, inside commands and tactics. + - Obtaining existing values from memory + - Composing values + - Verifying types + - Using these terms in commands + - Using these terms in tactics + - Automatic proofs without tactics using type classes and canonical structures + + compilation and loading must be performed as for `tuto0`. diff --git a/doc/plugin_tutorial/tuto0/Makefile b/doc/plugin_tutorial/tuto0/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto0/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto0/_CoqProject b/doc/plugin_tutorial/tuto0/_CoqProject new file mode 100644 index 0000000000..76368e3ac7 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/_CoqProject @@ -0,0 +1,10 @@ +-R theories/ Tuto0 +-I src + +theories/Loader.v +theories/Demo.v + +src/tuto0_main.ml +src/tuto0_main.mli +src/g_tuto0.mlg +src/tuto0_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto0/src/dune b/doc/plugin_tutorial/tuto0/src/dune new file mode 100644 index 0000000000..79d561061d --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/dune @@ -0,0 +1,9 @@ +(library + (name tuto0_plugin) + (public_name coq.plugins.tutorial.p0) + (libraries coq.plugins.ltac)) + +(rule + (targets g_tuto0.ml) + (deps (:pp-file g_tuto0.mlg) ) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg new file mode 100644 index 0000000000..5c633fe862 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg @@ -0,0 +1,18 @@ +DECLARE PLUGIN "tuto0_plugin" + +{ + +open Pp +open Ltac_plugin + +} + +VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY +| [ "HelloWorld" ] -> { Feedback.msg_notice (strbrk Tuto0_main.message) } +END + +TACTIC EXTEND hello_world_tactic +| [ "hello_world" ] -> + { let _ = Feedback.msg_notice (str Tuto0_main.message) in + Tacticals.New.tclIDTAC } +END diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_main.ml b/doc/plugin_tutorial/tuto0/src/tuto0_main.ml new file mode 100644 index 0000000000..93a807a800 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/tuto0_main.ml @@ -0,0 +1 @@ +let message = "Hello world!" diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_main.mli b/doc/plugin_tutorial/tuto0/src/tuto0_main.mli new file mode 100644 index 0000000000..846af3ed8c --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/tuto0_main.mli @@ -0,0 +1 @@ +val message : string diff --git a/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack b/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack new file mode 100644 index 0000000000..73be1bb561 --- /dev/null +++ b/doc/plugin_tutorial/tuto0/src/tuto0_plugin.mlpack @@ -0,0 +1,2 @@ +Tuto0_main +G_tuto0 diff --git a/doc/plugin_tutorial/tuto0/theories/Demo.v b/doc/plugin_tutorial/tuto0/theories/Demo.v new file mode 100644 index 0000000000..bdc61986af --- /dev/null +++ b/doc/plugin_tutorial/tuto0/theories/Demo.v @@ -0,0 +1,8 @@ +From Tuto0 Require Import Loader. + +HelloWorld. + +Lemma test : True. +Proof. +hello_world. +Abort. diff --git a/doc/plugin_tutorial/tuto0/theories/Loader.v b/doc/plugin_tutorial/tuto0/theories/Loader.v new file mode 100644 index 0000000000..7bce38382b --- /dev/null +++ b/doc/plugin_tutorial/tuto0/theories/Loader.v @@ -0,0 +1 @@ +Declare ML Module "tuto0_plugin". diff --git a/doc/plugin_tutorial/tuto1/Makefile b/doc/plugin_tutorial/tuto1/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto1/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto1/_CoqProject b/doc/plugin_tutorial/tuto1/_CoqProject new file mode 100644 index 0000000000..585d1360be --- /dev/null +++ b/doc/plugin_tutorial/tuto1/_CoqProject @@ -0,0 +1,13 @@ +-R theories Tuto1 +-I src + +theories/Loader.v + +src/simple_check.mli +src/simple_check.ml +src/simple_declare.mli +src/simple_declare.ml +src/simple_print.ml +src/simple_print.mli +src/g_tuto1.mlg +src/tuto1_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto1/src/dune b/doc/plugin_tutorial/tuto1/src/dune new file mode 100644 index 0000000000..cf9c674b14 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/dune @@ -0,0 +1,9 @@ +(library + (name tuto1_plugin) + (public_name coq.plugins.tutorial.p1) + (libraries coq.plugins.ltac)) + +(rule + (targets g_tuto1.ml) + (deps (:pp-file g_tuto1.mlg) ) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg new file mode 100644 index 0000000000..4df284d2d9 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -0,0 +1,154 @@ +DECLARE PLUGIN "tuto1_plugin" + +{ + +(* If we forget this line and include our own tactic definition using + TACTIC EXTEND, as below, then we get the strange error message + no implementation available for Tacentries, only when compiling + theories/Loader.v +*) +open Ltac_plugin +open Attributes +open Pp +(* This module defines the types of arguments to be used in the + EXTEND directives below, for example the string one. *) +open Stdarg + +} + +VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY +| [ "Hello" string(s) ] -> + { Feedback.msg_notice (strbrk "Hello " ++ str s) } +END + +(* reference is allowed as a syntactic entry, but so are all the entries + found the signature of module Prim in file coq/parsing/pcoq.mli *) + +VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY +| [ "HelloAgain" reference(r)] -> +(* The function Ppconstr.pr_qualid was found by searching all mli files + for a function of type qualid -> Pp.t *) + { Feedback.msg_notice + (strbrk "Hello again " ++ Ppconstr.pr_qualid r)} +END + +(* According to parsing/pcoq.mli, e has type constr_expr *) +(* this type is defined in pretyping/constrexpr.ml *) +(* Question for the developers: why is the file constrexpr.ml and not + constrexpr.mli --> Easier for packing the software in components. *) +VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY +| [ "Cmd1" constr(e) ] -> + { let _ = e in Feedback.msg_notice (strbrk "Cmd1 parsed something") } +END + +(* The next step is to make something of parsed expression. + Interesting information in interp/constrintern.mli *) + +(* There are several phases of transforming a parsed expression into + the final internal data-type (constr). There exists a collection of + functions that combine all the phases *) + +VERNAC COMMAND EXTEND TakingConstr2 CLASSIFIED AS QUERY +| [ "Cmd2" constr(e) ] -> + { let _ = Constrintern.interp_constr + (Global.env()) + (* Make sure you don't use Evd.empty here, as this does not + check consistency with existing universe constraints. *) + (Evd.from_env (Global.env())) e in + Feedback.msg_notice (strbrk "Cmd2 parsed something legitimate") } +END + +(* This is to show what happens when typing in an empty environment + with an empty evd. + Question for the developers: why does "Cmd3 (fun x : nat => x)." + raise an anomaly, not the same error as "Cmd3 (fun x : a => x)." *) + +VERNAC COMMAND EXTEND TakingConstr3 CLASSIFIED AS QUERY +| [ "Cmd3" constr(e) ] -> + { let _ = Constrintern.interp_constr Environ.empty_env + Evd.empty e in + Feedback.msg_notice + (strbrk "Cmd3 accepted something in the empty context")} +END + +(* When adding a definition, we have to be careful that just + the operation of constructing a well-typed term may already change + the environment, at the level of universe constraints (which + are recorded in the evd component). The function + Constrintern.interp_constr ignores this side-effect, so it should + not be used here. *) + +(* Looking at the interface file interp/constrintern.ml4, I lost + some time because I did not see that the "constr" type appearing + there was "EConstr.constr" and not "Constr.constr". *) + +VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF +| #[ poly = polymorphic ] [ "Cmd4" ident(i) constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + Simple_declare.packed_declare_definition ~poly i v } +END + +VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY +| [ "Cmd5" constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + let (_, ctx) = v in + let evd = Evd.from_ctx ctx in + Feedback.msg_notice + (Printer.pr_econstr_env (Global.env()) evd + (Simple_check.simple_check1 v)) } +END + +VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY +| [ "Cmd6" constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + let evd, ty = Simple_check.simple_check2 v in + Feedback.msg_notice + (Printer.pr_econstr_env (Global.env()) evd ty) } +END + +VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY +| [ "Cmd7" constr(e) ] -> + { let v = Constrintern.interp_constr (Global.env()) + (Evd.from_env (Global.env())) e in + let (a, ctx) = v in + let evd = Evd.from_ctx ctx in + Feedback.msg_notice + (Printer.pr_econstr_env (Global.env()) evd + (Simple_check.simple_check3 v)) } +END + +(* This command takes a name and return its value. It does less + than Print, because it fails on constructors, axioms, and inductive types. + This should be improved, because the error message is an anomaly. + Anomalies should never appear even when using a command outside of its + intended use. *) +VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY +| [ "Cmd8" reference(r) ] -> + { let env = Global.env() in + let evd = Evd.from_env env in + Feedback.msg_notice + (Printer.pr_econstr_env env evd + (EConstr.of_constr + (Simple_print.simple_body_access (Nametab.global r)))) } +END + +TACTIC EXTEND my_intro +| [ "my_intro" ident(i) ] -> + { Tactics.introduction i } +END + +(* if one write this: + VERNAC COMMAND EXTEND exploreproof CLASSIFIED AS QUERY + it gives an error message that is basically impossible to understand. *) + +VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY +| [ "Cmd9" ] -> + { let p = Proof_global.give_me_the_proof () in + let sigma, env = Pfedit.get_current_context () in + let pprf = Proof.partial_proof p in + Feedback.msg_notice + (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) } +END diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml new file mode 100644 index 0000000000..1f636c531a --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml @@ -0,0 +1,32 @@ +let simple_check1 value_with_constraints = + begin + let evalue, st = value_with_constraints in + let evd = Evd.from_ctx st in +(* This is reverse engineered from vernacentries.ml *) +(* The point of renaming is to make sure the bound names printed by Check + can be re-used in `apply with` tactics that use bound names to + refer to arguments. *) + let j = Termops.on_judgment EConstr.of_constr + (Arguments_renaming.rename_typing (Global.env()) + (EConstr.to_constr evd evalue)) in + let {Environ.uj_type=x}=j in x + end + +let simple_check2 value_with_constraints = + let evalue, st = value_with_constraints in + let evd = Evd.from_ctx st in +(* This version should be preferred if bound variable names are not so + important, you want to really verify that the input is well-typed, + and if you want to obtain the type. *) +(* Note that the output value is a pair containing a new evar_map: + typing will fill out blanks in the term by add evar bindings. *) + Typing.type_of (Global.env()) evd evalue + +let simple_check3 value_with_constraints = + let evalue, st = value_with_constraints in + let evd = Evd.from_ctx st in +(* This version should be preferred if bound variable names are not so + important and you already expect the input to have been type-checked + before. Set ~lax to false if you want an anomaly to be raised in + case of a type error. Otherwise a ReTypeError exception is raised. *) + Retyping.get_type_of ~lax:true (Global.env()) evd evalue diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.mli b/doc/plugin_tutorial/tuto1/src/simple_check.mli new file mode 100644 index 0000000000..bcf1bf56cf --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_check.mli @@ -0,0 +1,8 @@ +val simple_check1 : + EConstr.constr Evd.in_evar_universe_context -> EConstr.constr + +val simple_check2 : + EConstr.constr Evd.in_evar_universe_context -> Evd.evar_map * EConstr.constr + +val simple_check3 : + EConstr.constr Evd.in_evar_universe_context -> EConstr.constr diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml new file mode 100644 index 0000000000..9d10a8ba72 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -0,0 +1,24 @@ +(* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *) +let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = + let sigma = Evd.minimize_universes sigma in + let body = EConstr.to_constr sigma body in + let tyopt = Option.map (EConstr.to_constr sigma) tyopt in + let uvars_fold uvars c = + Univ.LSet.union uvars (Vars.universes_of_constr c) in + let uvars = List.fold_left uvars_fold Univ.LSet.empty + (Option.List.cons tyopt [body]) in + let sigma = Evd.restrict_universe_context sigma uvars in + let univs = Evd.check_univ_decl ~poly sigma udecl in + let ubinders = Evd.universe_binders sigma in + let ce = Declare.definition_entry ?types:tyopt ~univs body in + DeclareDef.declare_definition ident k ce ubinders imps ~hook + +let packed_declare_definition ~poly ident value_with_constraints = + let body, ctx = value_with_constraints in + let sigma = Evd.from_ctx ctx in + let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in + let udecl = UState.default_univ_decl in + let nohook = Lemmas.mk_hook (fun _ x -> ()) in + ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook) + +(* But this definition cannot be undone by Reset ident *) diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.mli b/doc/plugin_tutorial/tuto1/src/simple_declare.mli new file mode 100644 index 0000000000..fd74e81526 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.mli @@ -0,0 +1,5 @@ +open Names +open EConstr + +val packed_declare_definition : + poly:bool -> Id.t -> constr Evd.in_evar_universe_context -> unit diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml new file mode 100644 index 0000000000..cfc38ff9c9 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -0,0 +1,17 @@ +(* A more advanced example of how to explore the structure of terms of + type constr is given in the coq-dpdgraph plugin. *) + +let simple_body_access gref = + match gref with + | Globnames.VarRef _ -> + failwith "variables are not covered in this example" + | Globnames.IndRef _ -> + failwith "inductive types are not covered in this example" + | Globnames.ConstructRef _ -> + failwith "constructors are not covered in this example" + | Globnames.ConstRef cst -> + let cb = Environ.lookup_constant cst (Global.env()) in + match Global.body_of_constant_body cb with + | Some(e, _) -> e + | None -> failwith "This term has no value" + diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.mli b/doc/plugin_tutorial/tuto1/src/simple_print.mli new file mode 100644 index 0000000000..254b56ff79 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/simple_print.mli @@ -0,0 +1 @@ +val simple_body_access : Names.GlobRef.t -> Constr.constr diff --git a/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack new file mode 100644 index 0000000000..a797a509e0 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack @@ -0,0 +1,4 @@ +Simple_check +Simple_declare +Simple_print +G_tuto1 diff --git a/doc/plugin_tutorial/tuto1/theories/Loader.v b/doc/plugin_tutorial/tuto1/theories/Loader.v new file mode 100644 index 0000000000..6e8e308b3f --- /dev/null +++ b/doc/plugin_tutorial/tuto1/theories/Loader.v @@ -0,0 +1 @@ +Declare ML Module "tuto1_plugin". diff --git a/doc/plugin_tutorial/tuto2/Makefile b/doc/plugin_tutorial/tuto2/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto2/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto2/_CoqProject b/doc/plugin_tutorial/tuto2/_CoqProject new file mode 100644 index 0000000000..cf9cb5cc26 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/_CoqProject @@ -0,0 +1,6 @@ +-R theories/ Tuto +-I src + +theories/Test.v +src/demo.mlg +src/demo_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto2/src/.gitignore b/doc/plugin_tutorial/tuto2/src/.gitignore new file mode 100644 index 0000000000..5b1b6a902e --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/.gitignore @@ -0,0 +1 @@ +/demo.ml diff --git a/doc/plugin_tutorial/tuto2/src/demo.mlg b/doc/plugin_tutorial/tuto2/src/demo.mlg new file mode 100644 index 0000000000..966c05acdc --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/demo.mlg @@ -0,0 +1,375 @@ +(* -------------------------------------------------------------------------- *) +(* *) +(* Initial ritual dance *) +(* *) +(* -------------------------------------------------------------------------- *) + +DECLARE PLUGIN "demo_plugin" + +(* + Use this macro before any of the other OCaml macros. + + Each plugin has a unique name. + We have decided to name this plugin as "demo_plugin". + That means that: + + (1) If we want to load this particular plugin to Coq toplevel, + we must use the following command. + + Declare ML Module "demo_plugin". + + (2) The above command will succeed only if there is "demo_plugin.cmxs" + in some of the directories that Coq is supposed to look + (i.e. the ones we specified via "-I ..." command line options). + + (3) The file "demo_plugin.mlpack" lists the OCaml modules to be linked in + "demo_plugin.cmxs". + + (4) The file "demo_plugin.mlpack" as well as all .ml, .mli and .mlg files + are listed in the "_CoqProject" file. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd1 CLASSIFIED AS QUERY +| [ "Cmd1" ] -> { () } +END + +(* + These: + + VERNAC COMMAND EXTEND + + and + + END + + mark the beginning and the end of the definition of a new Vernacular command. + + Cmd1 is a unique identifier (which must start with an upper-case letter) + associated with the new Vernacular command we are defining. + + CLASSIFIED AS QUERY tells Coq that the new Vernacular command: + - changes neither the global environment + - nor does it modify the plugin's state. + + If the new command could: + - change the global environment + - or modify a plugin's state + then one would have to use CLASSIFIED AS SIDEFF instead. + + This: + + [ "Cmd1" ] -> { () } + + defines: + - the parsing rule + - the interpretation rule + + The parsing rule and the interpretation rule are separated by -> token. + + The parsing rule, in this case, is: + + [ "Cmd1" ] + + By convention, all vernacular command start with an upper-case letter. + + The [ and ] characters mark the beginning and the end of the parsing rule. + The parsing rule itself says that the syntax of the newly defined command + is composed from a single terminal Cmd1. + + The interpretation rule, in this case, is: + + { () } + + Similarly to the case of the parsing rule, + { and } characters mark the beginning and the end of the interpretation rule. + In this case, the following Ocaml expression: + + () + + defines the effect of the Vernacular command we have just defined. + That is, it behaves is no-op. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with some terminal parameters? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd2 CLASSIFIED AS QUERY +| [ "Cmd2" "With" "Some" "Terminal" "Parameters" ] -> { () } +END + +(* + As shown above, the Vernacular command can be composed from + any number of terminals. + + By convention, each of these terminals starts with an upper-case letter. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with some non-terminal parameter? *) +(* *) +(* -------------------------------------------------------------------------- *) + +{ + +open Stdarg + +} + +VERNAC COMMAND EXTEND Cmd3 CLASSIFIED AS QUERY +| [ "Cmd3" int(i) ] -> { () } +END + +(* + This: + + open Stdarg + + is needed as some identifiers in the Ocaml code generated by the + + VERNAC COMMAND EXTEND ... END + + macros are not fully qualified. + + This: + + int(i) + + means that the new command is expected to be followed by an integer. + The integer is bound in the parsing rule to variable i. + This variable i then can be used in the interpretation rule. + + To see value of which Ocaml types can be bound this way, + look at the wit_* function declared in interp/stdarg.mli + (in the Coq's codebase). + + If we drop the wit_ prefix, we will get the token + that we can use in the parsing rule. + That is, since there exists wit_int, we know that + we can write: + + int(i) + + By looking at the signature of the wit_int function: + + val wit_int : int uniform_genarg_type + + we also know that variable i will have the type int. + + The types of wit_* functions are either: + + 'c uniform_genarg_type + + or + + ('a,'b,'c) genarg_type + + In both cases, the bound variable will have type 'c. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command with variable number of arguments? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd4 CLASSIFIED AS QUERY +| [ "Cmd4" int_list(l) ] -> { () } +END + +(* + This: + + int_list(l) + + means that the new Vernacular command is expected to be followed + by a (whitespace separated) list of integers. + This list of integers is bound to the indicated l. + + In this case, as well as in the cases we point out below, instead of int + in int_list we could use any other supported type, e.g. ident, bool, ... + + To see which other Ocaml type constructors (in addition to list) + are supported, have a look at the parse_user_entry function defined + in grammar/q_util.mlp file. + + E.g.: + - ne_int_list(x) would represent a non-empty list of integers, + - int_list(x) would represent a list of integers, + - int_opt(x) would represent a value of type int option, + - ··· +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to define a new Vernacular command that takes values of a custom type? *) +(* *) +(* -------------------------------------------------------------------------- *) + +{ + +open Ltac_plugin + +} + +(* + If we want to avoid a compilation failure + + "no implementation available for Tacenv" + + then we have to open the Ltac_plugin module. +*) + +(* + Pp module must be opened because some of the macros that are part of the API + do not expand to fully qualified names. +*) + +{ + +type type_5 = Foo_5 | Bar_5 + +} + +(* + We define a type of values that we want to pass to our Vernacular command. +*) + +(* + By default, we are able to define new Vernacular commands that can take + parameters of some of the supported types. Which types are supported, + that was discussed earlier. + + If we want to be able to define Vernacular command that takes parameters + of a type that is not supported by default, we must use the following macro: +*) + +{ + +open Pp + +} + +VERNAC ARGUMENT EXTEND custom5 +| [ "Foo_5" ] -> { Foo_5 } +| [ "Bar_5" ] -> { Bar_5 } +END + +(* + where: + + custom5 + + indicates that, from now on, in our parsing rules we can write: + + custom5(some_variable) + + in those places where we expect user to provide an input + that can be parsed by the parsing rules above + (and interpreted by the interpretations rules above). +*) + +(* Here: *) + +VERNAC COMMAND EXTEND Cmd5 CLASSIFIED AS QUERY +| [ "Cmd5" custom5(x) ] -> { () } +END + +(* + we define a new Vernacular command whose parameters, provided by the user, + can be mapped to values of type_5. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to give a feedback to the user? *) +(* *) +(* -------------------------------------------------------------------------- *) + +VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY +| [ "Cmd6" ] -> { Feedback.msg_notice (Pp.str "Everything is awesome!") } +END + +(* + The following functions: + + - Feedback.msg_info : Pp.t -> unit + - Feedback.msg_notice : Pp.t -> unit + - Feedback.msg_warning : Pp.t -> unit + - Feedback.msg_error : Pp.t -> unit + - Feedback.msg_debug : Pp.t -> unit + + enable us to give user a textual feedback. + + Pp module enable us to represent and construct pretty-printing instructions. + The concepts defined and the services provided by the Pp module are in + various respects related to the concepts and services provided + by the Format module that is part of the Ocaml standard library. +*) + +(* -------------------------------------------------------------------------- *) +(* *) +(* How to implement a Vernacular command with (undoable) side-effects? *) +(* *) +(* -------------------------------------------------------------------------- *) + +{ + +open Summary.Local + +} + +(* + By opening Summary.Local module we shadow the original functions + that we traditionally use for implementing stateful behavior. + + ref + ! + := + + are now shadowed by their counterparts in Summary.Local. *) + +{ + +let counter = ref ~name:"counter" 0 + +} + +VERNAC COMMAND EXTEND Cmd7 CLASSIFIED AS SIDEFF +| [ "Cmd7" ] -> { counter := succ !counter; + Feedback.msg_notice (Pp.str "counter = " ++ Pp.str (string_of_int (!counter))) } +END + +TACTIC EXTEND tactic1 +| [ "tactic1" ] -> { Proofview.tclUNIT () } +END + +(* ---- *) + +{ + +type custom = Foo_2 | Bar_2 + +let pr_custom _ _ _ = function + | Foo_2 -> Pp.str "Foo_2" + | Bar_2 -> Pp.str "Bar_2" + +} + +ARGUMENT EXTEND custom2 PRINTED BY { pr_custom } +| [ "Foo_2" ] -> { Foo_2 } +| [ "Bar_2" ] -> { Bar_2 } +END + +TACTIC EXTEND tactic2 +| [ "tactic2" custom2(x) ] -> { Proofview.tclUNIT () } +END diff --git a/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack b/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack new file mode 100644 index 0000000000..4f0b8480b5 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/demo_plugin.mlpack @@ -0,0 +1 @@ +Demo diff --git a/doc/plugin_tutorial/tuto2/src/dune b/doc/plugin_tutorial/tuto2/src/dune new file mode 100644 index 0000000000..f2bc405455 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/src/dune @@ -0,0 +1,9 @@ +(library + (name tuto2_plugin) + (public_name coq.plugins.tutorial.p2) + (libraries coq.plugins.ltac)) + +(rule + (targets demo.ml) + (deps (:pp-file demo.mlg) ) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto2/theories/Test.v b/doc/plugin_tutorial/tuto2/theories/Test.v new file mode 100644 index 0000000000..38e83bfff1 --- /dev/null +++ b/doc/plugin_tutorial/tuto2/theories/Test.v @@ -0,0 +1,19 @@ +Declare ML Module "demo_plugin". + +Cmd1. +Cmd2 With Some Terminal Parameters. +Cmd3 42. +Cmd4 100 200 300 400. +Cmd5 Foo_5. +Cmd5 Bar_5. +Cmd6. +Cmd7. +Cmd7. +Cmd7. + +Goal True. +Proof. + tactic1. + tactic2 Foo_2. + tactic2 Bar_2. +Abort. diff --git a/doc/plugin_tutorial/tuto3/Makefile b/doc/plugin_tutorial/tuto3/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/doc/plugin_tutorial/tuto3/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/doc/plugin_tutorial/tuto3/_CoqProject b/doc/plugin_tutorial/tuto3/_CoqProject new file mode 100644 index 0000000000..e2a60a430f --- /dev/null +++ b/doc/plugin_tutorial/tuto3/_CoqProject @@ -0,0 +1,12 @@ +-R theories Tuto3 +-I src + +theories/Data.v +theories/Loader.v + +src/tuto_tactic.ml +src/tuto_tactic.mli +src/construction_game.ml +src/construction_game.mli +src/g_tuto3.mlg +src/tuto3_plugin.mlpack diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.ml b/doc/plugin_tutorial/tuto3/src/construction_game.ml new file mode 100644 index 0000000000..9d9f894e18 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/construction_game.ml @@ -0,0 +1,186 @@ +open Pp + +let find_reference = Coqlib.find_reference [@ocaml.warning "-3"] + +let example_sort evd = +(* creating a new sort requires that universes should be recorded + in the evd datastructure, so this datastructure also needs to be + passed around. *) + let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in + let new_type = EConstr.mkSort s in + evd, new_type + +let c_one evd = +(* In the general case, global references may refer to universe polymorphic + objects, and their universe has to be made afresh when creating an instance. *) + let gr_S = + find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in +(* the long name of "S" was found with the command "About S." *) + let gr_O = + find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in + let evd, c_O = Evarutil.new_global evd gr_O in + let evd, c_S = Evarutil.new_global evd gr_S in +(* Here is the construction of a new term by applying functions to argument. *) + evd, EConstr.mkApp (c_S, [| c_O |]) + +let dangling_identity env evd = +(* I call this a dangling identity, because it is not polymorph, but + the type on which it applies is left unspecified, as it is + represented by an existential variable. The declaration for this + existential variable needs to be added in the evd datastructure. *) + let evd, type_type = example_sort evd in + let evd, arg_type = Evarutil.new_evar env evd type_type in +(* Notice the use of a De Bruijn index for the inner occurrence of the + bound variable. *) + evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type, + EConstr.mkRel 1) + +let dangling_identity2 env evd = +(* This example uses directly a function that produces an evar that + is meant to be a type. *) + let evd, (arg_type, type_type) = + Evarutil.new_type_evar env evd Evd.univ_rigid in + evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type, + EConstr.mkRel 1) + +let example_sort_app_lambda () = + let env = Global.env () in + let evd = Evd.from_env env in + let evd, c_v = c_one evd in +(* dangling_identity and dangling_identity2 can be used interchangeably here *) + let evd, c_f = dangling_identity2 env evd in + let c_1 = EConstr.mkApp (c_f, [| c_v |]) in + let _ = Feedback.msg_notice + (Printer.pr_econstr_env env evd c_1) in + (* type verification happens here. Type verification will update + existential variable information in the evd part. *) + let evd, the_type = Typing.type_of env evd c_1 in +(* At display time, you will notice that the system knows about the + existential variable being instantiated to the "nat" type, even + though c_1 still contains the meta-variable. *) + Feedback.msg_notice + ((Printer.pr_econstr_env env evd c_1) ++ + str " has type " ++ + (Printer.pr_econstr_env env evd the_type)) + + +let c_S evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in + Evarutil.new_global evd gr + +let c_O evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in + Evarutil.new_global evd gr + +let c_E evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in + Evarutil.new_global evd gr + +let c_D evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in + Evarutil.new_global evd gr + +let c_Q evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in + Evarutil.new_global evd gr + +let c_R evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in + Evarutil.new_global evd gr + +let c_N evd = + let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in + Evarutil.new_global evd gr + +let c_C evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "C" in + Evarutil.new_global evd gr + +let c_F evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in + Evarutil.new_global evd gr + +let c_P evd = + let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in + Evarutil.new_global evd gr + +(* If c_S was universe polymorphic, we should have created a new constant + at each iteration of buildup. *) +let mk_nat evd n = + let evd, c_S = c_S evd in + let evd, c_O = c_O evd in + let rec buildup = function + | 0 -> c_O + | n -> EConstr.mkApp (c_S, [| buildup (n - 1) |]) in + if n <= 0 then evd, c_O else evd, buildup n + +let example_classes n = + let env = Global.env () in + let evd = Evd.from_env env in + let evd, c_n = mk_nat evd n in + let evd, n_half = mk_nat evd (n / 2) in + let evd, c_N = c_N evd in + let evd, c_div = c_D evd in + let evd, c_even = c_E evd in + let evd, c_Q = c_Q evd in + let evd, c_R = c_R evd in + let arg_type = EConstr.mkApp (c_even, [| c_n |]) in + let evd0 = evd in + let evd, instance = Evarutil.new_evar env evd arg_type in + let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in + let evd, the_type = Typing.type_of env evd c_half in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in + let proved_equality = + EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), Constr.DEFAULTcast, + EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in +(* This is where we force the system to compute with type classes. *) +(* Question to coq developers: why do we pass two evd arguments to + solve_remaining_evars? Is the choice of evd0 relevant here? *) + let evd = Pretyping.solve_remaining_evars + (Pretyping.default_inference_flags true) env evd ~initial:evd0 in + let evd, final_type = Typing.type_of env evd proved_equality in + Feedback.msg_notice (Printer.pr_econstr_env env evd proved_equality) + +(* This function, together with definitions in Data.v, shows how to + trigger automatic proofs at the time of typechecking, based on + canonical structures. + + n is a number for which we want to find the half (and a proof that + this half is indeed the half) +*) +let example_canonical n = + let env = Global.env () in + let evd = Evd.from_env env in +(* Construct a natural representation of this integer. *) + let evd, c_n = mk_nat evd n in +(* terms for "nat", "eq", "S_ev", "eq_refl", "C" *) + let evd, c_N = c_N evd in + let evd, c_F = c_F evd in + let evd, c_R = c_R evd in + let evd, c_C = c_C evd in + let evd, c_P = c_P evd in +(* the last argument of C *) + let refl_term = EConstr.mkApp (c_R, [|c_N; c_n |]) in +(* Now we build two existential variables, for the value of the half and for + the "S_ev" structure that triggers the proof search. *) + let evd, ev1 = Evarutil.new_evar env evd c_N in +(* This is the type for the second existential variable *) + let csev = EConstr.mkApp (c_F, [| ev1 |]) in + let evd, ev2 = Evarutil.new_evar env evd csev in +(* Now we build the C structure. *) + let test_term = EConstr.mkApp (c_C, [| c_n; ev1; ev2; refl_term |]) in +(* Type-checking this term will compute values for the existential variables *) + let evd, final_type = Typing.type_of env evd test_term in +(* The computed type has two parameters, the second one is the proof. *) + let value = match EConstr.kind evd final_type with + | Constr.App(_, [| _; the_half |]) -> the_half + | _ -> failwith "expecting the whole type to be \"cmp _ the_half\"" in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd value) in +(* I wish for a nicer way to get the value of ev2 in the evar_map *) + let prf_struct = EConstr.of_constr (EConstr.to_constr evd ev2) in + let the_prf = EConstr.mkApp (c_P, [| ev1; prf_struct |]) in + let evd, the_statement = Typing.type_of env evd the_prf in + Feedback.msg_notice + (Printer.pr_econstr_env env evd the_prf ++ str " has type " ++ + Printer.pr_econstr_env env evd the_statement) diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.mli b/doc/plugin_tutorial/tuto3/src/construction_game.mli new file mode 100644 index 0000000000..1832ed6630 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/construction_game.mli @@ -0,0 +1,4 @@ +val dangling_identity : Environ.env -> Evd.evar_map -> Evd.evar_map * EConstr.t +val example_sort_app_lambda : unit -> unit +val example_classes : int -> unit +val example_canonical : int -> unit diff --git a/doc/plugin_tutorial/tuto3/src/dune b/doc/plugin_tutorial/tuto3/src/dune new file mode 100644 index 0000000000..ba6d8b288f --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/dune @@ -0,0 +1,10 @@ +(library + (name tuto3_plugin) + (public_name coq.plugins.tutorial.p3) + (flags :standard -warn-error -3) + (libraries coq.plugins.ltac)) + +(rule + (targets g_tuto3.ml) + (deps (:pp-file g_tuto3.mlg)) + (action (run coqpp %{pp-file}))) diff --git a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg new file mode 100644 index 0000000000..82ba45726e --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg @@ -0,0 +1,46 @@ +DECLARE PLUGIN "tuto3_plugin" + +{ + +open Ltac_plugin + +open Construction_game + +(* This one is necessary, to avoid message about missing wit_string *) +open Stdarg + +} + +VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY +| [ "Tuto3_1" ] -> + { let env = Global.env () in + let evd = Evd.from_env env in + let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in + let new_type_2 = EConstr.mkSort s in + let evd, _ = + Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in + Feedback.msg_notice + (Printer.pr_econstr_env env evd new_type_2) } +END + +VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY +| [ "Tuto3_2" ] -> { example_sort_app_lambda () } +END + +TACTIC EXTEND collapse_hyps +| [ "pack" "hypothesis" ident(i) ] -> + { Tuto_tactic.pack_tactic i } +END + +(* More advanced examples, where automatic proof happens but + no tactic is being called explicitely. The first one uses + type classes. *) +VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY +| [ "Tuto3_3" int(n) ] -> { example_classes n } +END + +(* The second one uses canonical structures. *) +VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY +| [ "Tuto3_4" int(n) ] -> { example_canonical n } +END + diff --git a/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack b/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack new file mode 100644 index 0000000000..f4645ad7ed --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/tuto3_plugin.mlpack @@ -0,0 +1,3 @@ +Construction_game +Tuto_tactic +G_tuto3 diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml new file mode 100644 index 0000000000..8f2c387d09 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml @@ -0,0 +1,143 @@ +open Proofview + +let constants = ref ([] : EConstr.t list) + +(* This is a pattern to collect terms from the Coq memory of valid terms + and proofs. This pattern extends all the way to the definition of function + c_U *) +let collect_constants () = + if (!constants = []) then + let open EConstr in + let open UnivGen in + let find_reference = Coqlib.find_reference [@ocaml.warning "-3"] in + let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "pack" in + let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "packer" in + let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in + let gr_P = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "prod" in + let gr_U = find_reference "Tuto3" ["Tuto3"; "Data"] "uncover" in + constants := List.map (fun x -> of_constr (constr_of_monomorphic_global x)) + [gr_H; gr_M; gr_R; gr_P; gr_U]; + !constants + else + !constants + +let c_H () = + match collect_constants () with + it :: _ -> it + | _ -> failwith "could not obtain an internal representation of pack" + +let c_M () = + match collect_constants () with + _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of pack_marker" + +let c_R () = + match collect_constants () with + _ :: _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of pair" + +let c_P () = + match collect_constants () with + _ :: _ :: _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of prod" + +let c_U () = + match collect_constants () with + _ :: _ :: _ :: _ :: it :: _ -> it + | _ -> failwith "could not obtain an internal representation of prod" + +(* The following tactic is meant to pack an hypothesis when no other + data is already packed. + + The main difficulty in defining this tactic is to understand how to + construct the input expected by apply_in. *) +let package i = Goal.enter begin fun gl -> + Tactics.apply_in true false i + [(* this means that the applied theorem is not to be cleared. *) + None, (CAst.make (c_M (), + (* we don't specialize the theorem with extra values. *) + Tactypes.NoBindings))] + (* we don't destruct the result according to any intro_pattern *) + None + end + +(* This function is meant to observe a type of shape (f a) + and return the value a. *) + +(* Remark by Maxime: look for destApp combinator. *) +let unpack_type evd term = + let report () = + CErrors.user_err (Pp.str "expecting a packed type") in + match EConstr.kind evd term with + | Constr.App (_, [| ty |]) -> ty + | _ -> report () + +(* This function is meant to observe a type of shape + A -> pack B -> C and return A, B, C + but it is not used in the current version of our tactic. + It is kept as an example. *) +let two_lambda_pattern evd term = + let report () = + CErrors.user_err (Pp.str "expecting two nested implications") in +(* Note that pattern-matching is always done through the EConstr.kind function, + which only provides one-level deep patterns. *) + match EConstr.kind evd term with + (* Here we recognize the outer implication *) + | Constr.Prod (_, ty1, l1) -> + (* Here we recognize the inner implication *) + (match EConstr.kind evd l1 with + | Constr.Prod (n2, packed_ty2, deep_conclusion) -> + (* Here we recognized that the second type is an application *) + ty1, unpack_type evd packed_ty2, deep_conclusion + | _ -> report ()) + | _ -> report () + +(* In the environment of the goal, we can get the type of an assumption + directly by a lookup. The other solution is to call a low-cost retyping + function like *) +let get_type_of_hyp env id = + match EConstr.lookup_named id env with + | Context.Named.Declaration.LocalAssum (_, ty) -> ty + | _ -> CErrors.user_err (let open Pp in + str (Names.Id.to_string id) ++ + str " is not a plain hypothesis") + +let repackage i h_hyps_id = Goal.enter begin fun gl -> + let env = Goal.env gl in + let evd = Tacmach.New.project gl in + let concl = Tacmach.New.pf_concl gl in + let (ty1 : EConstr.t) = get_type_of_hyp env i in + let (packed_ty2 : EConstr.t) = get_type_of_hyp env h_hyps_id in + let ty2 = unpack_type evd packed_ty2 in + let new_packed_type = EConstr.mkApp (c_P (), [| ty1; ty2 |]) in + let open EConstr in + let new_packed_value = + mkApp (c_R (), [| ty1; ty2; mkVar i; + mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in + Refine.refine ~typecheck:true begin fun evd -> + let evd, new_goal = Evarutil.new_evar env evd + (mkProd (Names.Name.Anonymous, + mkApp(c_H (), [| new_packed_type |]), + Vars.lift 1 concl)) in + evd, mkApp (new_goal, + [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |]) + end + end + +let pack_tactic i = + let h_hyps_id = (Names.Id.of_string "packed_hyps") in + Proofview.Goal.enter begin fun gl -> + let hyps = Environ.named_context_val (Proofview.Goal.env gl) in + if not (Termops.mem_named_context_val i hyps) then + (CErrors.user_err + (Pp.str ("no hypothesis named" ^ (Names.Id.to_string i)))) + else + if Termops.mem_named_context_val h_hyps_id hyps then + tclTHEN (repackage i h_hyps_id) + (tclTHEN (Tactics.clear [h_hyps_id; i]) + (Tactics.introduction h_hyps_id)) + else + tclTHEN (package i) + (tclTHEN (Tactics.rename_hyp [i, h_hyps_id]) + (Tactics.move_hyp h_hyps_id Logic.MoveLast)) + end diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli b/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli new file mode 100644 index 0000000000..dbf6cf48e2 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.mli @@ -0,0 +1,3 @@ +val two_lambda_pattern : + Evd.evar_map -> EConstr.t -> EConstr.t * EConstr.t * EConstr.t +val pack_tactic : Names.Id.t -> unit Proofview.tactic diff --git a/doc/plugin_tutorial/tuto3/theories/Data.v b/doc/plugin_tutorial/tuto3/theories/Data.v new file mode 100644 index 0000000000..f7395d686b --- /dev/null +++ b/doc/plugin_tutorial/tuto3/theories/Data.v @@ -0,0 +1,73 @@ + + +Inductive pack (A: Type) : Type := + packer : A -> pack A. + +Arguments packer {A}. + +Definition uncover (A : Type) (packed : pack A) : A := + match packed with packer v => v end. + +Notation "!!!" := (pack _) (at level 0, only printing). + +(* The following data is used as material for automatic proofs + based on type classes. *) + +Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}. + +Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}. + +Lemma even_rec n h : 2 * h = n -> 2 * S h = S (S n). +Proof. + intros []. + simpl. rewrite <-plus_n_O, <-plus_n_Sm. + reflexivity. +Qed. + +Instance EvenNat_rec n (p : EvenNat n) : EvenNat (S (S n)) := + {half := S (@half _ p); half_prop := even_rec n (@half _ p) (@half_prop _ p)}. + +Definition tuto_div2 n (p : EvenNat n) := @half _ p. + +(* to be used in the following examples +Compute (@half 8 _). + +Check (@half_prop 8 _). + +Check (@half_prop 7 _). + +and in command Tuto3_3 8. *) + +(* The following data is used as material for automatic proofs + based on canonical structures. *) + +Record S_ev n := Build_S_ev {double_of : nat; _ : 2 * n = double_of}. + +Definition s_half_proof n (r : S_ev n) : 2 * n = double_of n r := + match r with Build_S_ev _ _ h => h end. + +Canonical Structure can_ev_default n d (Pd : 2 * n = d) : S_ev n := + Build_S_ev n d Pd. + +Canonical Structure can_ev0 : S_ev 0 := + Build_S_ev 0 0 (@eq_refl _ 0). + +Lemma can_ev_rec n : forall (s : S_ev n), S_ev (S n). +Proof. +intros s; exists (S (S (double_of _ s))). +destruct s as [a P]. +exact (even_rec _ _ P). +Defined. + +Canonical Structure can_ev_rec. + +Record cmp (n : nat) (k : nat) := + C {h : S_ev k; _ : double_of k h = n}. + +(* To be used in, e.g., + +Check (C _ _ _ eq_refl : cmp 6 _). + +Check (C _ _ _ eq_refl : cmp 7 _). + +*) diff --git a/doc/plugin_tutorial/tuto3/theories/Loader.v b/doc/plugin_tutorial/tuto3/theories/Loader.v new file mode 100644 index 0000000000..1351cff63b --- /dev/null +++ b/doc/plugin_tutorial/tuto3/theories/Loader.v @@ -0,0 +1,3 @@ +From Tuto3 Require Export Data. + +Declare ML Module "tuto3_plugin". diff --git a/doc/plugin_tutorial/tuto3/theories/test.v b/doc/plugin_tutorial/tuto3/theories/test.v new file mode 100644 index 0000000000..43204ddf34 --- /dev/null +++ b/doc/plugin_tutorial/tuto3/theories/test.v @@ -0,0 +1,23 @@ +(* to be used e.g. in : coqtop -I src -R theories Tuto3 < theories/test.v *) + +Require Import Tuto3.Loader. + +(* This should print Type. *) +Tuto3_1. + +(* This should print a term that contains an existential variable. *) +(* And then print the same term, where the variable has been correctly + instantiated. *) +Tuto3_2. + +Lemma tutu x y (A : 0 < x) (B : 10 < y) : True. +Proof. +pack hypothesis A. +(* Hypothesis A should have disappeared and a "packed_hyps" hypothesis + should have appeared, with unreadable content. *) +pack hypothesis B. +(* Hypothesis B should have disappeared *) +destruct packed_hyps as [unpacked_hyps]. +(* Hypothesis unpacked_hyps should contain the previous contents of A and B. *) +exact I. +Qed. diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 827b7c13c1..067af954ad 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -1189,7 +1189,6 @@ def setup(app): app.connect('doctree-resolved', CoqtopBlocksTransform.merge_consecutive_coqtop_blocks) # Add extra styles - app.add_stylesheet("fonts.css") app.add_stylesheet("ansi.css") app.add_stylesheet("coqdoc.css") app.add_javascript("notations.js") diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 7bc5d090b4..95a0039b0a 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -293,9 +293,6 @@ let ids_of_pattern_list = (List.fold_left (cases_pattern_fold_names Id.Set.add)) Id.Set.empty -let ids_of_cases_indtype p = - cases_pattern_fold_names Id.Set.add Id.Set.empty p - let ids_of_cases_tomatch tms = List.fold_right (fun (_, ona, indnal) l -> diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 8c735edfc9..f1a8ed202f 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -113,9 +113,6 @@ val map_constr_expr_with_binders : val replace_vars_constr_expr : Id.t Id.Map.t -> constr_expr -> constr_expr -(** Specific function for interning "in indtype" syntax of "match" *) -val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t - val free_vars_of_constr_expr : constr_expr -> Id.Set.t val occur_var_constr_expr : Id.t -> constr_expr -> bool diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7aa85a0810..c8c38ffe05 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -573,12 +573,17 @@ let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id = (* TODO binders *) next_ident_away_from id (fun id -> Id.Set.mem id fvs3) -let is_var store pat = +let is_patvar c = + match DAst.get c with + | PatVar _ -> true + | _ -> false + +let is_patvar_store store pat = match DAst.get pat with | PatVar na -> ignore(store na); true | _ -> false -let out_var pat = +let out_patvar pat = match pat.v with | CPatAtom (Some qid) when qualid_is_ident qid -> Name (qualid_basename qid) @@ -600,7 +605,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam let pat = coerce_to_cases_pattern_expr (fst (Id.Map.find id terms)) in let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in let pat, na = match disjpat with - | [pat] when is_var store pat -> let na = get () in None, na + | [pat] when is_patvar_store store pat -> let na = get () in None, na | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in (renaming,env), pat, na with Not_found -> @@ -610,7 +615,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam let env = set_env_scopes env scopes in if onlyident then (* Do not try to interpret a variable as a constructor *) - let na = out_var pat in + let na = out_patvar pat in let env = push_name_env ntnvars (Variable,[],[],[]) env (make ?loc:pat.loc na) in (renaming,env), None, na else @@ -618,7 +623,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in let pat, na = match disjpat with - | [pat] when is_var store pat -> let na = get () in None, na + | [pat] when is_patvar_store store pat -> let na = get () in None, na | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in (renaming,env), pat, na with Not_found -> @@ -743,7 +748,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in if onlyident then - let na = out_var c in term_of_name na, None + let na = out_patvar c in term_of_name na, None else let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in match disjpat with @@ -805,7 +810,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = (* and since we are only interested in the pattern as a term *) let env = reset_hidden_inductive_implicit_test env in if onlyident then - term_of_name (out_var pat) + term_of_name (out_patvar pat) else let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in match disjpat with @@ -1741,7 +1746,7 @@ let intern_ind_pattern genv ntnvars scopes pat = let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in (with_letin, match product_of_cases_patterns empty_alias idslpl with - | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin) + | ids,[asubst,pl] -> (c,ids,asubst,chop_params_pattern loc c pl with_letin) | _ -> error_bad_inductive_type ?loc) | x -> error_bad_inductive_type ?loc @@ -1979,30 +1984,30 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = end | CCases (sty, rtnpo, tms, eqns) -> let as_in_vars = List.fold_left (fun acc (_,na,inb) -> - Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc) - (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na) - inb) Id.Set.empty tms in + (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na)) + Id.Set.empty tms in (* as, in & return vars *) let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in - let tms,ex_ids,match_from_in = List.fold_right - (fun citm (inds,ex_ids,matchs) -> - let ((tm,ind),extra_id,match_td) = intern_case_item env forbidden_vars citm in - (tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs) - tms ([],Id.Set.empty,[]) in + let tms,ex_ids,aliases,match_from_in = List.fold_right + (fun citm (inds,ex_ids,asubst,matchs) -> + let ((tm,ind),extra_id,(ind_ids,alias_subst,match_td)) = + intern_case_item env forbidden_vars citm in + (tm,ind)::inds, + Id.Set.union ind_ids (Option.fold_right Id.Set.add extra_id ex_ids), + merge_subst alias_subst asubst, + List.rev_append match_td matchs) + tms ([],Id.Set.empty,Id.Map.empty,[]) in let env' = Id.Set.fold (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var)) (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in (* PatVars before a real pattern do not need to be matched *) let stripped_match_from_in = - let is_patvar c = match DAst.get c with - | PatVar _ -> true - | _ -> false - in let rec aux = function | [] -> [] | (_, c) :: q when is_patvar c -> aux q | l -> l in aux match_from_in in + let rtnpo = Option.map (replace_vars_constr_expr aliases) rtnpo in let rtnpo = match stripped_match_from_in with | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *) | l -> @@ -2150,7 +2155,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* the "in" part *) let match_td,typ = match t with | Some t -> - let with_letin,(ind,l) = intern_ind_pattern globalenv ntnvars (None,env.scopes) t in + let with_letin,(ind,ind_ids,alias_subst,l) = + intern_ind_pattern globalenv ntnvars (None,env.scopes) t in let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in (* for "in Vect n", we answer (["n","n"],[(loc,"n")]) @@ -2186,9 +2192,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let _,args_rel = List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in canonize_args args_rel l forbidden_names_for_gen [] [] in - match_to_do, Some (CAst.make ?loc:(cases_pattern_expr_loc t) (ind,List.rev_map (fun x -> x.v) nal)) + (Id.Set.of_list (List.map (fun id -> id.CAst.v) ind_ids),alias_subst,match_to_do), + Some (CAst.make ?loc:(cases_pattern_expr_loc t) (ind,List.rev_map (fun x -> x.v) nal)) | None -> - [], None in + (Id.Set.empty,Id.Map.empty,[]), None in (tm',(na.CAst.v, typ)), extra_id, match_td and intern_impargs c env l subscopes args = diff --git a/kernel/names.ml b/kernel/names.ml index b2d6a489a6..9f27212967 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -391,6 +391,8 @@ module KerName = struct let print kn = str (to_string kn) + let debug_print kn = str (debug_to_string kn) + let compare (kn1 : kernel_name) (kn2 : kernel_name) = if kn1 == kn2 then 0 else diff --git a/kernel/names.mli b/kernel/names.mli index 350db871d5..61df3bad0e 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -149,15 +149,15 @@ sig val is_empty : t -> bool (** Test whether a directory path is empty. *) - val to_string : t -> string - (** Print directory paths as ["coq_root.module.submodule"] *) - val initial : t (** Initial "seed" of the unique identifier generator *) val hcons : t -> t (** Hashconsing of directory paths. *) + val to_string : t -> string + (** Print non-empty directory paths as ["coq_root.module.submodule"] *) + val print : t -> Pp.t end @@ -180,15 +180,15 @@ sig val make : string -> t (** Create a label out of a string. *) - val to_string : t -> string - (** Conversion to string. *) - val of_id : Id.t -> t (** Conversion from an identifier. *) val to_id : t -> Id.t (** Conversion to an identifier. *) + val to_string : t -> string + (** Conversion to string. *) + val print : t -> Pp.t (** Pretty-printer. *) @@ -227,10 +227,10 @@ sig (** Return the identifier contained in the argument. *) val to_string : t -> string - (** Conversion to a string. *) + (** Encode as a string (not to be used for user-facing messages). *) val debug_to_string : t -> string - (** Same as [to_string], but outputs information related to debug. *) + (** Same as [to_string], but outputs extra information related to debug. *) end @@ -252,16 +252,17 @@ sig val is_bound : t -> bool - val to_string : t -> string - - val debug_to_string : t -> string - (** Same as [to_string], but outputs information related to debug. *) - val initial : t (** Name of the toplevel structure ([= MPfile initial_dir]) *) val dp : t -> DirPath.t + val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + + val debug_to_string : t -> string + (** Same as [to_string], but outputs extra information related to debug. *) + end module MPset : Set.S with type elt = ModPath.t @@ -284,13 +285,17 @@ sig val modpath : t -> ModPath.t val label : t -> Label.t - (** Display *) val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + + val print : t -> Pp.t + (** Print internal representation (not to be used for user-facing messages). *) val debug_to_string : t -> string - (** Same as [to_string], but outputs information related to debug. *) + (** Same as [to_string], but outputs extra information related to debug. *) - val print : t -> Pp.t + val debug_print : t -> Pp.t + (** Same as [print], but outputs extra information related to debug. *) (** Comparisons *) val compare : t -> t -> int @@ -365,9 +370,16 @@ sig (** Displaying *) val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + val print : t -> Pp.t + (** Print internal representation (not to be used for user-facing messages). *) + val debug_to_string : t -> string + (** Same as [to_string], but outputs extra information related to debug. *) + val debug_print : t -> Pp.t + (** Same as [print], but outputs extra information related to debug. *) end @@ -444,9 +456,16 @@ sig (** Displaying *) val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + val print : t -> Pp.t + (** Print internal representation (not to be used for user-facing messages). *) + val debug_to_string : t -> string + (** Same as [to_string], but outputs extra information related to debug. *) + val debug_print : t -> Pp.t + (** Same as [print], but outputs extra information related to debug. *) end @@ -567,8 +586,12 @@ module Projection : sig val map : (MutInd.t -> MutInd.t) -> t -> t val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t - val print : t -> Pp.t val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + + val print : t -> Pp.t + (** Print internal representation (not to be used for user-facing messages). *) + end type t (* = Repr.t * bool *) @@ -609,7 +632,10 @@ module Projection : sig val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t val to_string : t -> string + (** Encode as a string (not to be used for user-facing messages). *) + val print : t -> Pp.t + (** Print internal representation (not to be used for user-facing messages). *) end diff --git a/lib/system.ml b/lib/system.ml index a9db95318f..fd6579dd69 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -287,20 +287,20 @@ let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) = real (round (sstop -. sstart)) ++ str "s" ++ str ")" -let with_time ~batch f x = +let with_time ~batch ~header f x = let tstart = get_time() in let msg = if batch then "" else "Finished transaction in " in try let y = f x in let tend = get_time() in let msg2 = if batch then "" else " (successful)" in - Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); y with e -> let tend = get_time() in let msg = if batch then "" else "Finished failing transaction in " in let msg2 = if batch then "" else " (failure)" in - Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e (* We use argv.[0] as we don't want to resolve symlinks *) diff --git a/lib/system.mli b/lib/system.mli index a3b79ee528..6dd1eb5a84 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -105,7 +105,7 @@ val time_difference : time -> time -> float (** in seconds *) val fmt_time_difference : time -> time -> Pp.t -val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b +val with_time : batch:bool -> header:Pp.t -> ('a -> 'b) -> 'a -> 'b (** [get_toplevel_path program] builds a complete path to the executable denoted by [program]. This involves: diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index f0bb6f58a6..ff2c900130 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -1,5 +1,14 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) open Goal open Environ diff --git a/plugins/ssrmatching/ssrmatching.v b/plugins/ssrmatching/ssrmatching.v index 9a53e1dd1a..a39f76db9e 100644 --- a/plugins/ssrmatching/ssrmatching.v +++ b/plugins/ssrmatching/ssrmatching.v @@ -1,5 +1,15 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) + Declare ML Module "ssrmatching_plugin". Module SsrMatchingSyntax. diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e6e1530e36..ed28cc7725 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -46,15 +46,10 @@ let () = Goptions.(declare_bool_option { (* Functions to deal with impossible cases *) (*******************************************) let impossible_default_case env = - let type_of_id = - let open Names.GlobRef in - match Coqlib.lib_ref "core.IDProp.type" with - | ConstRef c -> c - | VarRef _ | IndRef _ | ConstructRef _ -> assert false - in + let type_of_id = Coqlib.lib_ref "core.IDProp.type" in let c, ctx = UnivGen.fresh_global_instance env (Coqlib.(lib_ref "core.IDProp.idProp")) in - let (_, u) = Constr.destConst c in - Some (c, Constr.mkConstU (type_of_id, u), ctx) + let (_, u) = Constr.destRef c in + Some (c, Constr.mkRef (type_of_id, u), ctx) let coq_unit_judge = let open Environ in diff --git a/stm/stm.ml b/stm/stm.ml index 32c6c7d959..169d608d2d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -869,7 +869,6 @@ end = struct (* {{{ *) cur_id := id | { state = Error ie } -> - cur_id := id; Exninfo.iraise ie | _ -> @@ -2017,7 +2016,7 @@ end = struct (* {{{ *) find ~time:false ~batch:false ~fail:false e in let st = Vernacstate.freeze_interp_state ~marshallable:false in Vernacentries.with_fail st fail (fun () -> - (if time then System.with_time ~batch else (fun x -> x)) (fun () -> + (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> let Proof.{goals} = Proof.data p in @@ -2832,17 +2831,9 @@ let merge_proof_branch ~valid ?id qast keep brname = (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) let handle_failure (e, info) vcs = - match Stateid.get info with - | None -> - VCS.restore vcs; - VCS.print (); - anomaly(str"error with no safe_id attached:" ++ spc() ++ - CErrors.iprint_no_report (e, info) ++ str".") - | Some (safe_id, id) -> - stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); - VCS.restore vcs; - VCS.print (); - Exninfo.iraise (e, info) + VCS.restore vcs; + VCS.print (); + Exninfo.iraise (e, info) let snapshot_vio ~doc ldir long_f_dot_vo = let doc = finish ~doc in @@ -2993,7 +2984,14 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) (* Unknown: we execute it, check for open goals and propagate sideeff *) | VtUnknown, VtNow -> let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in - let id = VCS.new_node ~id:newtip () in + if not (get_allow_nested_proofs ()) && in_proof then + "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on." + |> Pp.str + |> (fun s -> (UserError (None, s), Exninfo.null)) + |> State.exn_on ~valid:Stateid.dummy Stateid.dummy + |> Exninfo.iraise + else + let id = VCS.new_node ~id:newtip () in let head_id = VCS.get_branch_pos head in let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *) let step () = diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f40b3e901b..454a4b66e7 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -214,6 +214,6 @@ let classify_vernac e = | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtNow - | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) + | (VtStartProof _ | VtUnknown), _ -> VtQuery, VtLater) in static_control_classifier e diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 64f19e1fd9..69c1d9bd23 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -95,6 +95,7 @@ let schedule_vio_checking j fs = done; let pid, ret = Unix.wait () in if ret <> Unix.WEXITED 0 then rc := 1; + Worker.kill (Pool.find pid !pool); pool := Pool.remove pid !pool; done; exit !rc @@ -124,6 +125,7 @@ let schedule_vio_compilation j fs = | s :: rest -> s :: filter_argv b rest in let prog = Sys.argv.(0) in let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in + let all_jobs = !jobs in let make_job () = let f, t = List.hd !jobs in jobs := List.tl !jobs; @@ -137,8 +139,15 @@ let schedule_vio_compilation j fs = done; let pid, ret = Unix.wait () in if ret <> Unix.WEXITED 0 then rc := 1; + Worker.kill (Pool.find pid !pool); pool := Pool.remove pid !pool; done; + if !rc = 0 then begin + (* set the access and last modification time of all files to the same t + * not to confuse make into thinking that some of them are outdated *) + let t = Unix.gettimeofday () in + List.iter (fun (f,_) -> Unix.utimes (f^".vo") t t) all_jobs; + end; exit !rc diff --git a/test-suite/Makefile b/test-suite/Makefile index 34a1900bbc..37091a49e5 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -36,9 +36,10 @@ include ../Makefile.common # easily overridden LIB := .. BIN := $(shell cd ..; pwd)/bin/ +COQFLAGS?= -coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite -coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite +coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite $(COQFLAGS) +coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS) coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite coqdoc := $(BIN)coqdoc coqtopbyte := $(BIN)coqtop.byte diff --git a/test-suite/bugs/closed/bug_8369.v b/test-suite/bugs/closed/bug_8369.v new file mode 100644 index 0000000000..9816954d0c --- /dev/null +++ b/test-suite/bugs/closed/bug_8369.v @@ -0,0 +1,3 @@ +(* Was failing in master with a not_found generated by the printer *) + +Fail Definition foo := fun '(u, v) p2 => (u, v). diff --git a/test-suite/bugs/closed/bug_9240.v b/test-suite/bugs/closed/bug_9240.v new file mode 100644 index 0000000000..e0901dc2d9 --- /dev/null +++ b/test-suite/bugs/closed/bug_9240.v @@ -0,0 +1,12 @@ +Register unit as core.IDProp.type. +Register tt as core.IDProp.idProp. + + +Inductive vec (A : Type) : nat -> Type := +| nil : vec A 0 +| cons : forall n : nat, A -> vec A n -> vec A (S n). + +Definition hd (A : Type) (n : nat) (v : vec A (S n)) : A := +match v in (vec _ (S n)) return A with +| cons _ _ h _ => h +end. (* assertion failure in evarconv *) diff --git a/test-suite/bugs/closed/bug_9300.v b/test-suite/bugs/closed/bug_9300.v new file mode 100644 index 0000000000..a80f3233a3 --- /dev/null +++ b/test-suite/bugs/closed/bug_9300.v @@ -0,0 +1,6 @@ +Existing Class True. + +Instance foo {n : nat} (x := I) : forall {b : bool} (s : nat * nat), True. auto. Defined. + +Fail Check foo (n := 3) true (s := (4 , 5)). +Check foo (n := 3) (b := true) (4 , 5). diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/opened/bug_3166.v index e1c29a954c..baf87631f0 100644 --- a/test-suite/bugs/opened/bug_3166.v +++ b/test-suite/bugs/opened/bug_3166.v @@ -81,3 +81,4 @@ Goal forall T (x y : T) (p : x = y), True. compute in H0. change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0. Fail pose proof (fun k => @eq_trans _ _ _ k H0). +Abort. diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/opened/bug_3754.v index a717bbe735..18820b1a4c 100644 --- a/test-suite/bugs/opened/bug_3754.v +++ b/test-suite/bugs/opened/bug_3754.v @@ -282,3 +282,4 @@ Defined. rewrite <- ap_p_pp; rewrite_moveL_Mp_p. Set Debug Tactic Unification. Fail rewrite (concat_Ap ff2). + Abort. diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v index 5c74addb62..78b2aa69b9 100644 --- a/test-suite/bugs/opened/bug_3890.v +++ b/test-suite/bugs/opened/bug_3890.v @@ -1,3 +1,5 @@ +Set Nested Proofs Allowed. + Class Foo. Class Bar := b : Type. diff --git a/test-suite/bugs/opened/bug_3938.v b/test-suite/bugs/opened/bug_3938.v index 2d0d1930f1..3c7c945ed8 100644 --- a/test-suite/bugs/opened/bug_3938.v +++ b/test-suite/bugs/opened/bug_3938.v @@ -4,3 +4,4 @@ Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b. intros a b f H. rewrite H. (* Toplevel input, characters 15-25: Anomaly: Evar ?X11 was not declared. Please report. *) +Abort. diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v index ae5d51bae8..b7c98aa134 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.v +++ b/test-suite/output-modulo-time/ltacprof_cutoff.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-profile-ltac") -*- *) +(* -*- coq-prog-args: ("-async-proofs" "off" "-profile-ltac") -*- *) Require Coq.ZArith.BinInt. Module WithIdTac. Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac). diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index cf2d5b2850..14c48e8fa0 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -9,10 +9,11 @@ The command has indeed failed with message: Ltac call to "instantiate ( (ident) := (lglob) )" failed. Instance is not well-typed in the environment of ?x. The command has indeed failed with message: -Cannot infer the domain of the type of f. +Cannot infer ?T in the partial instance "?T -> nat" found for the type of f. The command has indeed failed with message: -Cannot infer the domain of the implicit parameter A of id whose type is -"Type". +Cannot infer ?T in the partial instance "?T -> nat" found for the implicit +parameter A of id whose type is "Type". The command has indeed failed with message: -Cannot infer the codomain of the type of f in environment: +Cannot infer ?T in the partial instance "forall x : nat, ?T" found for the +type of f in environment: x : nat diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 52fe98ac07..232ac17cbf 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -1873,3 +1873,12 @@ Check match niln in listn O return O=O with niln => eq_refl end. (* (was failing up to May 2017) *) Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end. + +(* A test about binding variables of "in" clause of "match" *) +(* (was failing from 8.5 to Dec 2018) *) + +Check match O in nat return nat with O => O | _ => O end. + +(* Checking that aliases are substituted in the correct order *) + +Check match eq_refl (1,0) in _ = (y as z, y' as z) return z = z with eq_refl => eq_refl end : 0=0. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 4372ac72ae..f8f10b34ae 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -126,6 +126,8 @@ TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line +TGTS ?= + ########## End of parameters ################################################## # What follows may be relevant to you only if you need to # extend this Makefile. If so, look for 'Extension point' here and @@ -237,6 +239,11 @@ vo_to_obj = $(addsuffix .o,\ $(filter-out Warning: Error:,\ $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) strip_dotslash = $(patsubst ./%,%,$(1)) + +# without this we get undefined variables in the expansion for the +# targets of the [deprecated,use-mllib-or-mlpack] rule +with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1))) + VO = vo VOFILES = $(VFILES:.v=.$(VO)) @@ -269,14 +276,14 @@ CMXSFILES = \ PACKEDFILES = \ $(call strip_dotslash, \ $(foreach lib, \ - $(call strip_dotslash, \ - $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$($(lib)))) + $(call strip_dotslash, \ + $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib)))) # files that are archived into a .cma (mllib) LIBEDFILES = \ $(call strip_dotslash, \ $(foreach lib, \ - $(call strip_dotslash, \ - $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$($(lib)))) + $(call strip_dotslash, \ + $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib)))) CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) OBJFILES = $(call vo_to_obj,$(VOFILES)) @@ -681,11 +688,11 @@ $(GHTMLFILES): %.g.html: %.v %.glob # Dependency files ############################################################ -ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) - -include $(ALLDFILES) -else - ifeq ($(MAKECMDGOALS),) +ifndef MAKECMDGOALS -include $(ALLDFILES) +else + ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) + -include $(ALLDFILES) endif endif @@ -784,3 +791,7 @@ debug: .PHONY: debug .DEFAULT_GOAL := all + +# Local Variables: +# mode: makefile-gmake +# End: diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index c914bbecff..d8465aac27 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -37,34 +37,6 @@ let vernac_echo ?loc in_chan = let open Loc in Feedback.msg_notice @@ str @@ really_input_string in_chan len ) loc -(* For coqtop -time, we display the position in the file, - and a glimpse of the executed command *) - -let pp_cmd_header {CAst.loc;v=com} = - let shorten s = - if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s - in - let noblank s = String.map (fun c -> - match c with - | ' ' | '\n' | '\t' | '\r' -> '~' - | x -> x - ) s - in - let (start,stop) = Option.cata Loc.unloc (0,0) loc in - let safe_pr_vernac x = - try Ppvernac.pr_vernac x - with e -> str (Printexc.to_string e) in - let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) - in str "Chars " ++ int start ++ str " - " ++ int stop ++ - str " [" ++ str cmd ++ str "] " - -(* This is a special case where we assume we are in console batch mode - and take control of the console. - *) -let print_cmd_header com = - Pp.pp_with !Topfmt.std_ft (pp_cmd_header com); - Format.pp_print_flush !Topfmt.std_ft () - (* Reenable when we get back to feedback printing *) (* let is_end_of_input any = match any with *) (* Stm.End_of_input -> true *) @@ -88,7 +60,6 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = due to the way it prints. *) let com = if state.time then begin - print_cmd_header com; CAst.make ?loc @@ VernacTime(state.time,com) end else com in let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com in diff --git a/vernac/classes.ml b/vernac/classes.ml index 370df615fc..a342f5bf98 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -301,10 +301,10 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~ if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) else tclass in - let sigma, k, u, cty, ctx', ctx, len, imps, subst = + let sigma, k, u, cty, ctx', ctx, imps, subst = let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in - let len = List.length ctx in + let len = Context.Rel.nhyps ctx in let imps = imps @ Impargs.lift_implicits len imps' in let ctx', c = decompose_prod_assum sigma c' in let ctx'' = ctx' @ ctx in @@ -320,7 +320,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~ | LocalDef (_,b,_) -> (args, Vars.substl args' b :: args')) cl_context (args, []) in - sigma, cl, u, c', ctx', ctx, len, imps, args + sigma, cl, u, c', ctx', ctx, imps, args in let id = match instid with diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a2b5c8d70a..f3e1e1fc49 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -511,7 +511,7 @@ let pr_trailing_ne_context_of env sigma = if List.is_empty (Environ.rel_context env) && List.is_empty (Environ.named_context env) then str "." - else (str " in environment:"++ pr_context_unlimited env sigma) + else (strbrk " in environment:" ++ pr_context_unlimited env sigma) let rec explain_evar_kind env sigma evk ty = let open Evar_kinds in @@ -551,21 +551,21 @@ let rec explain_evar_kind env sigma evk ty = strbrk "an instance of type " ++ ty ++ str " for the variable " ++ Id.print id | Evar_kinds.SubEvar (where,evk') -> - let evi = Evd.find sigma evk' in + let rec find_source evk = + let evi = Evd.find sigma evk in + match snd evi.evar_source with + | Evar_kinds.SubEvar (_,evk) -> find_source evk + | src -> evi,src in + let evi,src = find_source evk' in let pc = match evi.evar_body with | Evar_defined c -> pr_leconstr_env env sigma c | Evar_empty -> assert false in let ty' = evi.evar_concl in - (match where with - | Some Evar_kinds.Body -> str "the body of " - | Some Evar_kinds.Domain -> str "the domain of " - | Some Evar_kinds.Codomain -> str "the codomain of " - | None -> - pr_existential_key sigma evk ++ str " of type " ++ ty ++ - str " in the partial instance " ++ pc ++ - str " found for ") ++ - explain_evar_kind env sigma evk' - (pr_leconstr_env env sigma ty') (snd evi.evar_source) + pr_existential_key sigma evk ++ + strbrk " in the partial instance " ++ pc ++ + strbrk " found for " ++ + explain_evar_kind env sigma evk + (pr_leconstr_env env sigma ty') src let explain_typeclass_resolution env sigma evi k = match Typeclasses.class_of_constr sigma evi.evar_concl with diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 4065bb9c1f..b4b893a3fd 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -406,3 +406,24 @@ let with_output_to_file fname func input = deep_ft := Util.pi3 old_fmt; close_out channel; Exninfo.iraise reraise + +(* For coqtop -time, we display the position in the file, + and a glimpse of the executed command *) + +let pr_cmd_header {CAst.loc;v=com} = + let shorten s = + if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s + in + let noblank s = String.map (fun c -> + match c with + | ' ' | '\n' | '\t' | '\r' -> '~' + | x -> x + ) s + in + let (start,stop) = Option.cata Loc.unloc (0,0) loc in + let safe_pr_vernac x = + try Ppvernac.pr_vernac x + with e -> str (Printexc.to_string e) in + let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) + in str "Chars " ++ int start ++ str " - " ++ int stop ++ + str " [" ++ str cmd ++ str "] " diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 0ddf474970..5f84c5edee 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -71,3 +71,4 @@ val print_err_exn : exn -> unit redirected to a file [file] *) val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b +val pr_cmd_header : Vernacexpr.vernac_control CAst.t -> Pp.t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e6e3db4beb..dbccea1117 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2388,8 +2388,9 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} = control v | VernacRedirect (s, {v}) -> Topfmt.with_output_to_file s control v - | VernacTime (batch, {v}) -> - System.with_time ~batch control v; + | VernacTime (batch, com) -> + let header = if batch then Topfmt.pr_cmd_header com else Pp.mt () in + System.with_time ~batch ~header control com.CAst.v; and aux ~atts : _ -> unit = function diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index b40bccf27e..61540024ef 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -36,7 +36,8 @@ let do_if_not_cached rf f v = let freeze_interp_state ~marshallable = { system = update_cache s_cache (States.freeze ~marshallable); proof = update_cache s_proof (Proof_global.freeze ~marshallable); - shallow = marshallable } + shallow = false; + } let unfreeze_interp_state { system; proof } = do_if_not_cached s_cache States.unfreeze system; |