diff options
Diffstat (limited to 'dev')
-rw-r--r-- | dev/README | 4 | ||||
-rw-r--r-- | dev/TODO | 22 | ||||
-rwxr-xr-x | dev/build/osx/make-macos-dmg.sh | 14 | ||||
-rwxr-xr-x | dev/ci/ci-coq-dpdgraph.sh | 2 | ||||
-rw-r--r-- | dev/db_printers.ml | 16 | ||||
-rw-r--r-- | dev/doc/api.txt | 10 | ||||
-rw-r--r-- | dev/doc/changes.txt | 3 | ||||
-rw-r--r-- | dev/doc/notes-on-conversion.v (renamed from dev/doc/notes-on-conversion) | 0 | ||||
-rw-r--r-- | dev/tools/Makefile.devel | 74 | ||||
-rw-r--r-- | dev/tools/Makefile.dir | 131 | ||||
-rw-r--r-- | dev/tools/Makefile.subdir | 7 | ||||
-rw-r--r-- | dev/v8-syntax/.gitignore | 6 | ||||
-rw-r--r-- | dev/v8-syntax/syntax-v8.tex | 2 |
13 files changed, 16 insertions, 275 deletions
diff --git a/dev/README b/dev/README index 814f60957..b446c3e97 100644 --- a/dev/README +++ b/dev/README @@ -40,10 +40,6 @@ Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) Other development tools (directory tools) ----------------------- -Makefile.dir: makefile dedicated to intensive work in a given directory -Makefile.subdir: makefile dedicated to intensive work in a given subdirectory -Makefile.devel: utilities to automatically launch coq in various states -Makefile.common: used by other Makefiles objects.el: various development utilities at emacs level anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from diff --git a/dev/TODO b/dev/TODO deleted file mode 100644 index e62ee6e53..000000000 --- a/dev/TODO +++ /dev/null @@ -1,22 +0,0 @@ - - o options de la ligne de commande - - reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml - - o arguments implicites - - les calculer une fois pour toutes à la déclaration (dans Declare) - et stocker cette information dans le in_variable, in_constant, etc. - - o Environnements compilés (type Environ.compiled_env) - - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?) - - o Efficacité - - utiliser DOPL plutôt que DOPN (sauf pour Case) - - batch mode => pas de undo, ni de reset - - conversion : déplier la constante la plus récente - - un cache pour type_of_const, type_of_inductive, type_of_constructor, - lookup_mind_specif - - o Toplevel - - parsing de la ligne de commande : utiliser Arg ??? - - diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh index b43ada907..cbe2a5186 100755 --- a/dev/build/osx/make-macos-dmg.sh +++ b/dev/build/osx/make-macos-dmg.sh @@ -4,19 +4,13 @@ set -e # Configuration setup -eval `opam config env` -make distclean OUTDIR=$PWD/_install DMGDIR=$PWD/_dmg -./configure -debug -prefix $OUTDIR -native-compiler no VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml) APP=bin/CoqIDE_${VERSION}.app # Create a .app file with CoqIDE -~/.local/bin/jhbuild run make -j -l2 $APP - -# Build Coq and run test-suite -make && make check +make -j $NJOBS -l2 $APP # Add Coq to the .app file make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq install-ide-toploop @@ -29,7 +23,9 @@ mkdir -p $DMGDIR ln -sf /Applications $DMGDIR/Applications cp -r $APP $DMGDIR +mkdir -p _build + # Temporary countermeasure to hdiutil error 5341 -head -c9703424 /dev/urandom > $DMGDIR/.padding +# head -c9703424 /dev/urandom > $DMGDIR/.padding -hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO CoqIDE_$VERSION.dmg +hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO _build/CoqIDE_$VERSION.dmg diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh index e8018158b..b610f7000 100755 --- a/dev/ci/ci-coq-dpdgraph.sh +++ b/dev/ci/ci-coq-dpdgraph.sh @@ -7,4 +7,4 @@ coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR} -( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make tests && (make tests | tee tmp.log) && (if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi) ) +( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make test-suite ) diff --git a/dev/db_printers.ml b/dev/db_printers.ml deleted file mode 100644 index f4b4a425e..000000000 --- a/dev/db_printers.ml +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -open Pp -open Names - -let pp s = pp (hov 0 s) - -let prid id = Format.print_string (Id.to_string id) -let prsp sp = Format.print_string (DirPath.to_string sp) - - diff --git a/dev/doc/api.txt b/dev/doc/api.txt deleted file mode 100644 index 5827257b5..000000000 --- a/dev/doc/api.txt +++ /dev/null @@ -1,10 +0,0 @@ -Recommendations in using the API: - -The type of terms: constr (see kernel/constr.ml and kernel/term.ml) - -- On type constr, the canonical equality on CIC (up to - alpha-conversion and cast removal) is Constr.equal -- The type constr is abstract, use mkRel, mkSort, etc. to build - elements in constr; use "kind_of_term" to analyze the head of a - constr; use destRel, destSort, etc. when the head constructor is - known diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index a48c491d3..0f1a28028 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -188,6 +188,9 @@ In Coqlib / reference location: - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase was very specific. Use tclPROGRESS instead. +- New (internal) tactical `tclINDEPENDENTL` that combined with enter_one allows + to iterate a non-unit tactic on all goals and access their returned values. + - The unsafe flag of the Refine.refine function and its variants has been renamed and dualized into typecheck and has been made mandatory. diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion.v index a81f170c6..a81f170c6 100644 --- a/dev/doc/notes-on-conversion +++ b/dev/doc/notes-on-conversion.v diff --git a/dev/tools/Makefile.devel b/dev/tools/Makefile.devel deleted file mode 100644 index ffdb1bdca..000000000 --- a/dev/tools/Makefile.devel +++ /dev/null @@ -1,74 +0,0 @@ -# to be linked to makefile (lowercase - takes precedence over Makefile) -# in main directory -# make devel in main directory should do this for you. - -TOPDIR=. -BASEDIR= - -SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel API - -default: usage noargument - -usage:: - @echo Usage: make \<target\> - @echo Targets are: - -usage:: - @echo " setup-devel -- set the devel makefile" -setup-devel: - @ln -sfv dev/tools/Makefile.devel makefile - @(for i in $(SOURCEDIRS); do \ - (cd $(TOPDIR)/$$i; ln -sfv ../dev/tools/Makefile.dir Makefile) \ - done) - - -usage:: - @echo " clean-devel -- clear all devel files" -clean-devel: - echo rm -f makefile .depend.devel - echo rm -f $(foreach dir,$(SOURCEDIRS), $(TOPDIR)/$(dir)/Makefile) - - -usage:: - @echo " coqtop -- make until the bytecode executable, make the link" -coqtop: bin/coqtop.byte - ln -sf bin/coqtop.byte coqtop - - -usage:: - @echo " quick -- make bytecode executable and states" -quick: - $(MAKE) states BEST=byte - -include Makefile - -include $(TOPDIR)/dev/tools/Makefile.common - -# this file is better described in dev/tools/Makefile.dir -include .depend.devel - -#if dev/tools/Makefile.local exists, it is included -ifneq ($(wildcard $(TOPDIR)/dev/tools/Makefile.local),) -include $(TOPDIR)/dev/tools/Makefile.local -endif - - -usage:: - @echo " total -- runs coqtop with all theories required" -total: - ledit ./bin/coqtop.byte $(foreach th,$(THEORIESVO),-require $(notdir $(basename $(th)))) - - -usage:: - @echo " run -- makes and runs bytecode coqtop using ledit and the history file" - @echo " if you want to pass arguments to coqtop, use make run ARG=<args>" -run: $(TOPDIR)/coqtop - ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop $(ARG) $(ARGS) - - -usage:: - @echo " vars -- echos commands to set COQTOP and COQBIN variables" -vars: - @(cd $(TOPDIR); \ - echo export COQTOP=`pwd`/ ; \ - echo export COQBIN=`pwd`/bin/ ) diff --git a/dev/tools/Makefile.dir b/dev/tools/Makefile.dir deleted file mode 100644 index 1a1bb90b4..000000000 --- a/dev/tools/Makefile.dir +++ /dev/null @@ -1,131 +0,0 @@ -# make a link to this file if you are working hard in one directory of Coq -# ln -s ../dev/tools/Makefile.dir Makefile -# if you are working in a sub/dir/ make a link to dev/tools/Makefile.subdir instead -# this Makefile provides many useful facilities to develop Coq -# it is not completely compatible with .ml4 files unfortunately - -ifndef TOPDIR -TOPDIR=.. -endif - -# this complicated thing should work for subsubdirs as well -BASEDIR=$(shell (dir=`pwd`; cd $(TOPDIR); top=`pwd`; echo $$dir | sed -e "s|$$top/||")) - -noargs: dir - -test-dir: - @echo TOPDIR=$(TOPDIR) - @echo BASEDIR=$(BASEDIR) - -include $(TOPDIR)/dev/tools/Makefile.common - -# make this directory -dir: - $(MAKE) -C $(TOPDIR) $(notdir $(BASEDIR)) - -# make all cmo's in this directory. Useful in case the main Makefile is not -# up-to-date -all: - @( ( for i in *.ml; do \ - echo -n $(BASEDIR)/`basename $$i .ml`.cmo "" ; \ - done; \ - for i in *.ml4; do \ - echo -n $(BASEDIR)/`basename $$i .ml4`.cmo "" ; \ - done ) \ - | xargs $(MAKE) -C $(TOPDIR) ) - -# lists all files that should be compiled in this directory -list: - @(for i in *.mli; do \ - ls -l `basename $$i .mli`.cmi; \ - done) - @(for i in *.ml; do \ - ls -l `basename $$i .ml`.cmo; \ - done) - @(for i in *.ml4; do \ - ls -l `basename $$i .ml4`.cmo; \ - done) - - -clean:: - rm -f *.cmi *.cmo *.cmx *.o - - -# if grammar.cmo files cannot be compiled and main .depend cannot be -# rebuilt, this is quite useful -depend: - (cd $(TOPDIR); ocamldep -I $(BASEDIR) $(BASEDIR)/*.ml $(BASEDIR)/*.mli > .depend.devel) - - -# displays the dependency graph of the current directory (vertically, -# unlike in doc/) -graph: - (ocamldep *.ml *.mli | ocamldot | dot -Tps | gv -) & - - -# the pretty entry draws a dependency graph marking red those nodes -# which do not have their .cmo files - -.INTERMEDIATE: depend.dot depend.2.dot -.PHONY: depend.ps - -depend.dot: - ocamldep *.ml *.mli | ocamldot > $@ - -depend.2.dot: depend.dot - (i=`cat $< | wc -l`; i=`expr $$i - 1`; head -n $$i $<) > $@ - (for ml in *.ml; do \ - base=`basename $$ml .ml`; \ - fst=`echo $$base | cut -c1 | tr [:lower:] [:upper:]`; \ - rest=`echo $$base | cut -c2-`; \ - name=`echo $$fst $$rest | tr -d " "`; \ - cmo=$$base.cmo; \ - if [ ! -e $$cmo ]; then \ - echo \"$$name\" [color=red]\; >> $@;\ - fi;\ - done;\ - echo } >> $@) - -depend.ps: depend.2.dot - dot -Tps $< > $@ - -clean:: - rm -f depend.ps - -pretty: depend.ps - (gv -spartan $<; rm $<) & -# gv -spartan $< & - - - -# generating file.ml.mli by tricking make to pass -i to ocamlc - -%.ml.mli: FORCE - @(cmo=`basename $@ .ml.mli`.cmo ; \ - mv -f $$cmo $$cmo.tmp ; \ - $(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-i > $@ ; \ - echo Generated interface file $@ ; \ - mv -f $$cmo.tmp $$cmo) - -%.annot: FORCE - @(cmo=`basename $@ .annot`.cmo ; \ - mv -f $$cmo $$cmo.tmp ; \ - $(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-dtypes ; \ - echo Generated annotation file $@ ; \ - mv -f $$cmo.tmp $$cmo) - -FORCE: - -clean:: - rm -f *.ml.mli - -# this is not perfect but mostly WORKS! It just calls the main makefile - -%.cmi: FORCE - $(MAKE) -C $(TOPDIR) $(BASEDIR)/$@ - -%.cmo: FORCE - $(MAKE) -C $(TOPDIR) $(BASEDIR)/$@ - -coqtop: - $(MAKE) -C $(TOPDIR) bin/coqtop.byte diff --git a/dev/tools/Makefile.subdir b/dev/tools/Makefile.subdir deleted file mode 100644 index cb914bd12..000000000 --- a/dev/tools/Makefile.subdir +++ /dev/null @@ -1,7 +0,0 @@ -# if you work in a sub/sub-rectory of Coq -# you should make a link to that makefile -# ln -s ../../dev/tools/Makefile.subdir Makefile -# in order to have all the facilities of dev/tools/Makefile.dir - -TOPDIR=../.. -include $(TOPDIR)/dev/tools/Makefile.dir diff --git a/dev/v8-syntax/.gitignore b/dev/v8-syntax/.gitignore new file mode 100644 index 000000000..89e3509b0 --- /dev/null +++ b/dev/v8-syntax/.gitignore @@ -0,0 +1,6 @@ +# byproducts of check-grammar +def +df +use +use-k +use-t diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index fa2864cec..6b7960c92 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -1158,7 +1158,7 @@ $$ \nlsep \TERM{Abort}~\NT{ident} \nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body} \nlsep \TERM{Qed} -\nlsep \TERM{Save}~\NT{ident}} +\nlsep \TERM{Save}~\NT{ident} \nlsep \TERM{Defined}~\OPT{\NT{ident}} \nlsep \TERM{Suspend} \nlsep \TERM{Resume}~\OPT{\NT{ident}} |