Merge remote-tracking branch 'OFFICIAL/master'

13 files changed, 724 insertions, 445 deletions

diff --git a/CHANGES b/CHANGES
index dca879b3..4ac96315 100644
--- a/CHANGES
+++ b/CHANGES
@@ -26,6 +26,12 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
     option `coq-compile-quick' or the subsection "11.3.3 Quick
     compilation and .vio Files" in the Coq reference manual.
 
+*** new option coq-compile-keep-going (in menu Coq -> Auto Compilation)
+
+    Similar to ``make -k'', with this option enabled, background
+    compilation does not stop at the first error but rather
+    continues as far as possible.
+
 *** bug fixes
     - avoid leaving partial files behind when compilation fails
     - 123: Parallel background compliation fails to execute some
diff --git a/Makefile b/Makefile
index 635b2dc7..bcdd1db1 100644
--- a/Makefile
+++ b/Makefile
@@ -18,9 +18,6 @@
 ## 
 ###########################################################################
 
-# Disable parallel build for now, to workaround the issue raised in PR #112
-.NOTPARALLEL:
-
 # Set this according to your version of Emacs.
 # NB: this is also used to set default install path names below.
 EMACS=$(shell if [ -z "`which emacs`" ]; then echo "Emacs executable not found"; exit 1; else echo emacs; fi)
@@ -39,7 +36,7 @@ DEST_PREFIX=$(DESTDIR)/usr
 PROVERS=acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell
 OTHER_ELISP=generic lib contrib/mmm
 ELISP_DIRS=${PROVERS} ${OTHER_ELISP}
-ELISP_EXTRAS=isar/interface isar/isartags
+ELISP_EXTRAS=
 EXTRA_DIRS = images
 
 DOC_FILES=AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README REGISTER doc/*.pdf
@@ -52,6 +49,9 @@ BATCHEMACS=${EMACS} --batch --no-site-file -q
 BASH_SCRIPTS = isar/interface bin/proofgeneral
 PERL_SCRIPTS = lego/legotags coq/coqtags isar/isartags
 # Scripts to edit path to PG
+# the scripts target (part of install) and the cleanscripts target
+# (part of clean) work only under the assumption that PG_SCRIPTS is a subset of
+# the union of BASH_SCRIPTS and PERL_SCRIPTS.
 PG_SCRIPTS = bin/proofgeneral
 
 # Scripts to install to bin directory
@@ -134,7 +134,7 @@ all:	compile
 ##
 ## Remove generated targets
 ##
-clean:	cleanpgscripts
+clean:	cleanscripts
 	rm -f $(ELC) .\#* */.\#* */.autotest.log */.profile.log
 	(cd doc; $(MAKE) clean)
 
@@ -233,48 +233,50 @@ doc.%: FORCE
 ##
 ## scripts: try to patch bash and perl scripts with correct paths
 ##
+.PHONY: scripts
 scripts: bashscripts perlscripts pgscripts
 
+.PHONY: bashscripts
 bashscripts:
-	@(bash="`which bash`"; \
+	(bash="`which bash`"; \
 	 if [ -z "$$bash" ]; then \
 	   echo "Could not find bash - bash paths not checked" >&2; \
 	   exit 0; \
 	 fi; \
 	 for i in $(BASH_SCRIPTS); do \
-	   sed "s|^#.*!.*/bin/bash.*$$|#!$$bash|" < $$i > .tmp \
-	   && cat .tmp > $$i; \
-	 done; \
-	 rm -f .tmp)
+	   sed -i.orig "s|^#.*!.*/bin/bash.*$$|#!$$bash|" $$i; \
+	 done)
 
+.PHONY: perlscripts
 perlscripts:
-	@(perl="`which perl`"; \
+	(perl="`which perl`"; \
 	 if [ -z "$$perl" ]; then \
 	   echo "Could not find perl - perl paths not checked" >&2; \
 	   exit 0; \
 	 fi; \
 	 for i in $(PERL_SCRIPTS); do \
-	   sed "s|^#.*!.*/bin/perl.*$$|#!$$perl|" < $$i > .tmp \
-	   && cat .tmp > $$i; \
-	 done; \
-	 rm -f .tmp)
+	   sed -i.orig "s|^#.*!.*/bin/perl.*$$|#!$$perl|" $$i; \
+	 done)
 
 # FIXME: this next edit is really for install case, shouldn't be made
 # just when user types 'make'
-pgscripts:
-	@(for i in $(PG_SCRIPTS); do \
-	   sed "s|PGHOMEDEFAULT=.*$$|PGHOMEDEFAULT=${DEST_ELISP}|" < $$i > .tmp \
-	   && cat .tmp > $$i; \
-	 done; \
-	 rm -f .tmp)
+.PHONY: pgscripts
+pgscripts: bashscripts perlscripts
+	(for i in $(PG_SCRIPTS); do \
+	   sed -i.rm "s|PGHOMEDEFAULT=.*$$|PGHOMEDEFAULT=${DEST_ELISP}|" $$i; \
+	 done)
 
 # Set PGHOME path in scripts back to default location.
-cleanpgscripts:
-	@(for i in $(PG_SCRIPTS); do \
-	   sed "s|PGHOMEDEFAULT=.*$$|PGHOMEDEFAULT=\$$HOME/ProofGeneral|" < $$i > .tmp \
-	   && cat .tmp > $$i; \
-	 done; \
-	 rm -f .tmp)
+.PHONY: cleanscripts
+cleanscripts:
+	(for i in $(PG_SCRIPTS) $(BASH_SCRIPTS) $(PERL_SCRIPTS); do \
+	   if [ -f $$i.rm ] ; then \
+	     rm -f $$i.rm; \
+	   fi; \
+	   if [ -f $$i.orig ] ; then \
+             mv -f $$i.orig $$i; \
+           fi; \
+	 done)
 
 ##
 ## Include developer's makefile if it exists here.
diff --git a/Makefile.devel b/Makefile.devel
index 39accdc8..bba2efef 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -13,12 +13,12 @@
 ##
 ##    make elisptidy	  - tidy up elisp files (run whitespace-cleanup)
 ##
-##    make ChangeLog	  - make ChangeLog from CVS sources 
+##    make ChangeLog	  - make ChangeLog from git log
 ##    make tags		  - update TAGS file for Elisp sources
 ##    make autoloads	  - update autoloads
 ##
-##    make tag		  - tag the CVS sources with CVS_RELEASENAME
-##    make untag	  - remove tag CVS_RELEASENAME from the sources 
+##    make tag		  - tag the sources with GIT_RELEASENAME
+##    make untag	  - remove tag GIT_RELEASENAME from the sources
 ##    make dist           - make a distribution from sources with above tag
 ##    make rpm		  - make RPM packages based on etc/ProofGeneral.spec
 ##    make pkg		  - make Emacs tar file packages (Tromey's package.el)
@@ -43,8 +43,8 @@
 ##
 ##   Use 'make releaseclean' if giving up, to remove temp dirs.
 ##
-##   NB: no facility to edit html to make a full release in this Makefile.  
-##   Edit download.html by hand, then run 
+##   NB: no facility to edit html to make a full release in this Makefile.
+##   Edit download.html by hand, then run
 ##
 ##      make releaseall VERSION=2.0
 ##
@@ -57,7 +57,7 @@
 ##
 ##
 ## $Id$
-## 
+##
 ###########################################################################
 
 ## TODO: could include prerel tag in web pages, and link using -latest
@@ -89,14 +89,14 @@ DEVELOPERS=\
 # PRERELEASE_PREFIX is used to match PRERELEASE_TAG in sed
 # line in tag target below, which edits $(DOWNLOADHTML)
 # The prereltag.txt is kept as a record in the distrib area
-# of the current pre-release version (currently not used explicitly 
+# of the current pre-release version (currently not used explicitly
 # anywhere for web pages/whatever).
 PRERELEASE_PREFIX=4\.4\.1~pre
 PRERELEASE_TAG=4.4.1~pre
 ### Formerly: PRERELEASE_TAG=4.4pre$(shell date "+%y%m%d")
 PREREL_TAG_FILE=prereltag.txt
 
-# Path to web pages in repository, used for automatically 
+# Path to web pages in repository, used for automatically
 # updating with release information.
 HTMLDIR=../web
 DOWNLOADHTMLS=devel.html
@@ -124,14 +124,9 @@ VERSIONFILE=proof-site.el
 # Full version number defaults to ordinary version number.
 FULLVERSION=$(VERSION)
 
-#   NB: CVS tags can't have points in them.  
-#   Substitute points for hyphens.
-CVS_VERSION=$(shell echo $(FULLVERSION) | sed 's/\./-/g')
-
-
 # Name of tar file and RPM file.
 RELEASENAME = $(NAME)-$(VERSION)
-CVS_RELEASENAME = Release-$(CVS_VERSION)
+GIT_RELEASENAME ?= v$(FULLVERSION)
 
 # Where to release (i.e. copy) a new distribution to.
 # This may be the final directory (local) or temporary directory.
@@ -141,16 +136,6 @@ RELEASEDIR = /tmp/proofgeneral-www
 # How to make the release "live".  (Could be "true" to do nothing).
 GOLIVE=rsync -e ssh -auv $(RELEASEDIR)/* ssh.inf.ed.ac.uk:/group/project/proofgeneral/web/releases/
 
-
-CVSNAME = ProofGeneral
-
-# Remote commands to use CVS in server mode and install files.
-# With these settings the build can be done remotely.
-# CVSROOT = :pserver:da@cvs.inf.ed.ac.uk:/disk/cvs/proofgen
-# FIXME: this command causes an error on some recursive calls, e.g. to do
-# make clean in a non cvs directory.
-CVSROOT=$(shell cat CVS/Root)
-
 # Emacs for batch compiling
 BATCHEMACS=$(EMACS) -batch -q -no-site-file
 
@@ -160,10 +145,10 @@ EMACSFLAGS=-q -no-site-file
 # GNU version of tar, please
 TAR=tar
 
-# Files not to include the distribution area or tarball 
+# Files not to include the distribution area or tarball
 UNFINISHED_ELISP=
-ETC_FILES=etc/lego etc/coq etc/demoisa etc/isa etc/isar etc/lego etc/patches etc/*.txt 
-NONDISTFILES=.cvsignore */.cvsignore Makefile.devel etc/trac etc/testsuite $(UNFINISHED_ELISP) $(ETC_FILES)
+ETC_FILES=etc/lego etc/coq etc/demoisa etc/isa etc/isar etc/lego etc/patches etc/*.txt
+NONDISTFILES=.gitignore */.gitignore Makefile.devel etc/trac etc/testsuite $(UNFINISHED_ELISP) $(ETC_FILES)
 DOCDISTFILES=ProofGeneral.info PG-adapting.info
 
 # Files not to include in the ordinary distribution tarball, but left
@@ -181,7 +166,7 @@ RELEASENAMETGZ = $(RELEASENAME).tgz
 RELEASENAMERPM = $(RELEASENAME)-1.noarch.rpm
 RELEASENAMEDMG = $(RELEASENAME).dmg
 
-# Where to install a distribution 
+# Where to install a distribution
 DISTINSTALLDIR=/usr/local/share/elisp/proofgeneral
 
 SUBDIRS=$(ELISP_DIRS) etc doc images
@@ -192,7 +177,7 @@ FORCE:
 
 # Targets to pre-compile for distribution
 # Warning: elisp files are incompatible across emacs versions!
-alldist:	distcompile distdocs 
+alldist:	distcompile distdocs
 
 
 ############################################################
@@ -212,37 +197,30 @@ tags:	$(EL) $(TAGS_EXTRAS)
 run.%:
 	$(EMACS) $(EMACSFLAGS) -l generic/proof-site.el -eval '(proof-visit-example-file "$*")'
 
-test.%:	
+test.%:
 	if [ -f "$*/$*-autotest.el" ]; then if $(EMACS) $(EMACSFLAGS) -l generic/proof-site.el $*/$*-autotest.el -f eval-current-buffer; then echo "Autotests for $* run successfully on `date`"; else cat $*/.autotest.log; echo "Autotests for $* ran with failures on `date`"; exit 1; fi; fi
 
-profile.%:	
+profile.%:
 	if [ -f "$*/$*-profiling.el" ]; then if $(EMACS) $(EMACSFLAGS) -l generic/proof-site.el $*/$*-profiling.el -f eval-current-buffer; then echo "Profiling for $* run successfully on `date`"; else echo "Profiling for $* ran with failures on `date`"; exit 1; fi; cat $*/.profile.log; fi
 
-testall.%: 
+testall.%:
 	for prover in ${PROVERS}; do $(MAKE) test.$$prover EMACS=$*; done
 
 
 ############################################################
 #
-# Add recent messages to ChangeLog.  CVSROOT must be set correctly.
+# Add recent messages to ChangeLog.
 #
 # FIXME: this duplicates entries made on the same day: we could do
 # with a way of cleaning the last day from the ChangeLog.
 #
-# Debian default path
-RCS2LOG=/usr/share/cvs/contrib/rcs2log
 ChangeLog:	FORCE
-	$(RCS2LOG) -h "inf.ed.ac.uk" $(DEVELOPERS) -r -b -i 4 | sed 's|/home/proofgen/src/ProofGeneral/||g' > ChangeLog.prefix
-	if [ -f ChangeLog ]; then mv ChangeLog ChangeLog.old; else echo > ChangeLog.old; fi
-	cat ChangeLog.prefix ChangeLog.old | sed 's|/disk/cvs/proofgen/ProofGeneral/||g' > ChangeLog
-	rm ChangeLog.prefix ChangeLog.old
+	git log --pretty="format:%ad %s" --date=short > ChangeLog
 
-logupdate:  ChangeLog.gz
-	cvs commit -m"Updated" ChangeLog.gz
 
 ############################################################
 #
-# Clean up intermediate files 
+# Clean up intermediate files
 #
 devclean: FORCE
 	@echo "***** CLEANING UP INTERMEDIATE FILES ****"
@@ -253,23 +231,14 @@ devclean: FORCE
 
 ############################################################
 #
-# Clean up intermediate files, all generated files 
-#  and Emacs backups, CVS temps
+# Clean up intermediate files, all generated files
+#  and Emacs backups.
 #
 distclean: devclean clean
 	@echo "***** CLEANING UP ALL JUNK FILES ****"
 	find . \( -name '*~' -o -name '#*#' -o -name '\.\#*' -o -name '\.*\.log' \) -print | xargs rm -f
 	(cd doc; $(MAKE) distclean)
 
-############################################################
-#
-# Clean up all non-cvs files.
-#
-cvsclean:	clean
-	@echo "***** CLEANING UP ALL NON-CVS FILES ****"
-#	rm -rf $(FILES_NONCVS)
-	(cd doc; $(MAKE) distclean)
-
 
 ############################################################
 #
@@ -309,51 +278,49 @@ distcompile: FORCE
 
 ############################################################
 ##
-## tag:    tag the CVS sources of working directory with CVS_RELEASENAME,
-##	   set version stamp in proof-site.el and ProofGeneral.spec 
+## tag:    tag the sources of working directory with GIT_RELEASENAME,
+##	   set version stamp in proof-site.el and ProofGeneral.spec
 ##         to VERSION, and edit $(DOWNLOADHTMLS)
 ##	   if VERSION matches PRERELEASE_TAG.
 ##
-tag:		
+tag:
 	@echo "*************************************************"
-	@echo " Tagging sources... (you must rerun if CVS source dirty)"
+	@echo " Tagging sources... "
 	@echo "*************************************************"
-# Update the sources, this is almost always what we want to do.
-	if [ -z "$(NOCVS)" ] && [ -n "`cvs -n -q update -Pd | grep '^[MC] '`" ]; then cvs update -Pd; exit 1; fi
+	if [ -z "$(NOCVS)" ]; then git fetch origin && git log --exit-code master...origin/master || exit 1; fi
 # Update version in proof-site.el
 	(cd generic; mv $(VERSIONFILE) $(VERSIONFILE).old; sed -e 's/defconst $(VERSIONVARIABLE) \".*\"/defconst $(VERSIONVARIABLE) \"Proof General Version $(FULLVERSION).\"/g' $(VERSIONFILE).old > $(VERSIONFILE); rm $(VERSIONFILE).old)
 # Tag ProofGeneral.spec
 	(cd etc; mv ProofGeneral.spec ProofGeneral.spec.old; sed -e 's/Version:.*$$/Version:	$(VERSION)/g' ProofGeneral.spec.old > ProofGeneral.spec; rm ProofGeneral.spec.old)
 # Edit $(DOWNLOADHTMLS) only for prereleases.
 # Careful: the sed command below relies on previous value of PRERELEASE_TAG.
-	if [ $(PRERELEASE_TAG) = $(VERSION) ]; then \
-	  (cd $(HTMLDIR); \
-	   for f in $(DOWNLOADHTMLS); do \
-		mv $$f $$f.old; \
-		sed -e 's|ProofGeneral\([emacselc-]*\)-$(PRERELEASE_PREFIX)......|ProofGeneral\1-$(PRERELEASE_TAG)|g' $$f.old > $$f; \
-		rm $$f.old; \
-	   done) \
-	fi
-	if [ -z "$(NOCVS)" ]; then cvs commit -m"Set version tag for new release." generic/$(VERSIONFILE) etc/ProofGeneral.spec; (cd $(HTMLDIR); cvs commit -m"Set version tag for new release." $(DOWNLOADHTMLS)); fi
-	if [ -z "$(NOCVS)" ]; then cvs tag -cF "$(CVS_RELEASENAME)"; fi
+#	if [ $(PRERELEASE_TAG) = $(VERSION) ]; then \
+#	  (cd $(HTMLDIR); \
+#	   for f in $(DOWNLOADHTMLS); do \
+#		mv $$f $$f.old; \
+#		sed -e 's|ProofGeneral\([emacselc-]*\)-$(PRERELEASE_PREFIX)......|ProofGeneral\1-$(PRERELEASE_TAG)|g' $$f.old > $$f; \
+#		rm $$f.old; \
+#	   done) \
+#	fi
+	if [ -z "$(NOCVS)" ]; then git add generic/$(VERSIONFILE) etc/ProofGeneral.spec && git commit -m"Set version tag for new release." ; fi
+	if [ -z "$(NOCVS)" ]; then git tag -a  "$(GIT_RELEASENAME)"; fi
 
 ############################################################
 ##
-## untag:  Remove the CVS_RELEASENAME tag from the CVS sources.
+## untag:  Remove the GIT_RELEASENAME tag from the sources.
 ##
 
 untag:
-	cvs tag -d "$(CVS_RELEASENAME)"
+	git tag -d "$(GIT_RELEASENAME)"
 
 ############################################################
 ##
 ## dist: make a distribution in DISTBUILDIR from CVS sources
-##       Builds for user-distribution, from sources tagged 
-##       with CVS_RELEASENAME.
+##       Builds for user-distribution, from sources tagged
+##       with GIT_RELEASENAME.
 ##	 Moves html files to parent directory, removes
 ##       non-distributed files.
-##	 (NB: lines in subshells here inherit CVSROOT settings from above)
-##	    
+##
 
 cvsexport:
 	@echo "*************************************************"
@@ -362,8 +329,7 @@ cvsexport:
 	rm -rf $(DISTBUILDIR)
 	mkdir -p $(DISTBUILDIR)
 	if [ -z "$(NOCVS)" ]; then \
-           (cd $(DISTBUILDIR); \
-	    cvs -d $(CVSROOT) export -kv -r "${CVS_RELEASENAME}" -d ${RELEASENAME} ${CVSNAME}) \
+	   git archive --format=tar --prefix=$(RELEASENAME)/ $(GIT_RELEASENAME) | (cd "$(DISTBUILDIR)" && tar xf -) \
 	else \
 	   mkdir -p $(DISTBUILDIR)/$(RELEASENAME); \
 	   cp -pr . $(DISTBUILDIR)/$(RELEASENAME); \
@@ -390,7 +356,7 @@ dist:	cvsexport
 	-(cd $(DISTBUILDIR); ls $(IGNOREDFILES) > ignoredfiles; echo ignoredfiles >> ignoredfiles)
 #	link the long name to short name for convenience of user
 	(cd $(DISTBUILDIR); ln -sf $(RELEASENAME) $(NAME))
-	$(TAR) cvzf $(DISTBUILDIR)/$(RELEASENAMETGZ) --directory $(DISTBUILDIR) --exclude-from $(DISTBUILDIR)/ignoredfiles $(RELEASENAME) $(NAME) 
+	$(TAR) cvzf $(DISTBUILDIR)/$(RELEASENAMETGZ) --directory $(DISTBUILDIR) --exclude-from $(DISTBUILDIR)/ignoredfiles $(RELEASENAME) $(NAME)
 #	remove temporary files made for tar/zip only
 	(cd $(DISTBUILDIR); rm -f ignoredfiles $(NAME))
 	@echo "*************************************************"
@@ -401,12 +367,12 @@ dist:	cvsexport
 ############################################################
 ##
 ## release:
-##     tag the CVS sources, and make a distribution.
+##     tag the sources, and make a distribution.
 ##     Then install the distribution in RELEASEDIR
 ##     WARNING: RELEASEDIR is not cleaned except to remove
 ##     links, but files there with same names will be overwritten.
 ##
-release: check distclean tag dist 
+release: check distclean tag dist
 	@echo "*************************************************"
 	@echo " Making release (installing tarball distributions)."
 	@echo "*************************************************"
@@ -425,16 +391,16 @@ release: check distclean tag dist
 ############################################################
 ##
 ## rpm:
-##     Build an RPM binary package from the recently made distribution 
+##     Build an RPM binary package from the recently made distribution
 ##     using the tarball.  (Any user could do this)
 ##
-##	  
+##
 
 # Temporary RPM topdir for building packages as non-root user.
 RPMTOPDIR=/tmp/$(NAME)-rpm
 RPMBUILD=rpmbuild --define '_topdir $(RPMTOPDIR)'
 
-rpm:	
+rpm:
 	rm -rf $(RPMTOPDIR)
 	mkdir -p $(RPMTOPDIR)/RPMS
 	mkdir -p $(RPMTOPDIR)/SPECS
@@ -447,8 +413,8 @@ rpm:
 ##
 ## pkg:
 ##     Build an Emacs .tar file package
-##	  
-PKGMOVES=doc/dir doc/ProofGeneral.info doc/PG-adapting.info 
+##
+PKGMOVES=doc/dir doc/ProofGeneral.info doc/PG-adapting.info
 PKGDELETES=obsolete etc doc
 # Emacs package version is fussy about non-numbers in version, have to make version
 # from date.
@@ -466,7 +432,7 @@ pkg:	cvsexport
 ##
 ## rpmrelease:
 ##     Build and install RPM package into RELEASEDIR.
-##	  
+##
 rpmrelease: rpm
 	cp -pf $(RPMTOPDIR)/RPMS/noarch/* $(RELEASEDIR)
 
@@ -476,9 +442,9 @@ rpmrelease: rpm
 ##     Build (on Linux) a Mac OS X dmg disk image file
 ##     This requires sudo powers for mounting, and
 ##     (on Ubuntu), packages hfsplus and hfsprogs
-##	  
+##
 DMGBUILD=$(DISTBUILDIR)/dmg
-dmg:	
+dmg:
 	rm -rf $(DMGBUILD)
 	mkdir -p $(DMGBUILD)
 	dd if=/dev/zero of=$(DISTBUILDIR)/$(RELEASENAMEDMG) bs=1 count=0 seek=16M
@@ -511,23 +477,23 @@ releaseclean:
 ## fakereleaseall:
 ##     Do everything, but don't access CVS.  Just for
 ##     testing on non-live system, really.
-##	  
-## 
-fakereleaseall: 
-	$(MAKE) -f Makefile.devel release releaseclean NOCVS="no" 
+## FIXME: does this still make sense now that git is used version control?
+##
+fakereleaseall:
+	$(MAKE) -f Makefile.devel release releaseclean NOCVS="no"
 
 ############################################################
 ##
 ## releaseall:
 ##     Do everything!  (EXCEPT: ChangeLog.gz update)
-##	  
+##
 releaseall: release releaseclean golive
 
 ############################################################
 ##
 ## golive:
 ##     Execute golive command.
-##	  
+##
 golive:
 	$(GOLIVE)
 	cd $(HTMLDIR); for f in $(DOWNLOADHTMLS); do $(MAKE) pub.$$f; done;
@@ -540,8 +506,8 @@ golive:
 ##     Do everything for a final release based on a pre-release.
 ##     Except editing download file.
 ##
-releasefinal: release releaseclean 
-# Link the latest version 
+releasefinal: release releaseclean
+# Link the latest version
 # 31.5.13: remove this link from tar file, it is unconventional
 #	(cd $(DISTBUILDIR); rm -f $(NAME); ln -sf $(RELEASENAME) $(NAME))
 
@@ -550,7 +516,7 @@ releasefinal: release releaseclean
 ##
 ## distinstall:
 ##     Do everything for a local release.
-##	  
+##
 distall: distclean tag dist distinstall releaseclean
 
 
@@ -573,7 +539,7 @@ distinstall:
 ############################################################
 #
 # links:
-#   
+#
 #   Make some handy links for developers.
 #
 links:
@@ -582,9 +548,9 @@ links:
 
 #################################################################
 ##
-## Reporting Makefile settings.  
+## Reporting Makefile settings.
 ##
-## Useful for debugging Makefile 
+## Useful for debugging Makefile
 
 show.%:
 	@echo $($*)
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 767d2a6e..534c013d 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -161,7 +161,15 @@ It was constructed with `proof-defstringset-fn'.")
       :active coq-compile-before-require
       :help ,(concat "Compile parallel in background or "
 		    "sequentially with blocking ProofGeneral.")]
-     ["no quick"
+     ["Keep going"
+      coq-compile-keep-going-toggle
+      :style toggle
+      :selected coq-compile-keep-going
+      :active (and coq-compile-before-require
+		   coq-compile-parallel-in-background)
+      :help ,(concat "Continue background compilation after "
+		     "the first error as far as possible")]
+    ["no quick"
       (customize-set-variable 'coq-compile-quick 'no-quick)
       :style radio
       :selected (eq coq-compile-quick 'no-quick)
@@ -195,7 +203,12 @@ It was constructed with `proof-defstringset-fn'.")
       :selected coq-confirm-external-compilation
       :active (and coq-compile-before-require
 		   (not (equal coq-compile-command "")))
-      :help "Confirm external compilation command, see `coq-compile-command'."])
+      :help "Confirm external compilation command, see `coq-compile-command'."]
+     ["Abort Background Compilation"
+      coq-par-emergency-cleanup
+      :active (and coq-compile-before-require
+		   coq-compile-parallel-in-background)
+      :help "Abort background compilation and kill all compilation processes."])
     ""
     ["Print..." coq-Print :help "With prefix arg (C-u): Set Printing All first"]
     ["Check..." coq-Check :help "With prefix arg (C-u): Set Printing All first"]
@@ -244,6 +257,8 @@ It was constructed with `proof-defstringset-fn'.")
      ["Unset Printing Coercions" coq-unset-printing-coercions t]
      ["Set Printing Synth" coq-set-printing-synth t]
      ["Unset Printing Synth" coq-unset-printing-synth t]
+     ["Set Printing Universes" coq-set-printing-universes t]
+     ["Unset Printing Universes" coq-unset-printing-universes t]
      ["Set Printing Wildcards" coq-set-printing-wildcards t]
      ["Unset Printing Wildcards" coq-unset-printing-wildcards t]
      ["Set Printing Width" coq-ask-adapt-printing-width-and-show t])
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 1f31c1d3..af3e70a4 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -234,6 +234,9 @@ quick-and-vio2vo Same as `quick-no-vio2vo', but start vio2vo processes
                  compilation while you are processing stuff far below the
                  last require. vio2vo compilation is done on a subset of
                  the available cores, see `coq-compile-vio2vo-percentage'.
+                 When `coq-compile-keep-going' is set, vio2vo compilation
+                 is scheduled for those files for which coqc compilation
+                 was successful.
 
                  Warning: This mode does only work when you process require
                  commands in batches. Slowly single-stepping through require's
@@ -261,6 +264,19 @@ ensure-vo        Ensure that all library dependencies are present as .vo
    (eq coq-compile-quick 'quick-no-vio2vo)
    (eq coq-compile-quick 'quick-and-vio2vo)))
 
+(defcustom coq-compile-keep-going t
+  "Continue compilation after the first error as far as possible.
+Similar to ``make -k'', with this option enabled, the background
+compilation continues after the first error as far as possible.
+With this option disabled, background compilation is
+immediately stopped after the first error.
+
+This option can be set/reset via menu
+`Coq -> Auto Compilation -> Keep going'.")
+
+;; define coq-compile-keep-going-toggle
+(proof-deftoggle coq-compile-keep-going)
+
 (defcustom coq-max-background-compilation-jobs 'all-cpus
   "Maximal number of parallel jobs, if parallel compilation is enabled.
 Use the number of available CPU cores if this is set to
@@ -404,18 +420,6 @@ or not."
   :safe (lambda (v) (every 'stringp v))
   :group 'coq-auto-compile)
 
-(defcustom coq-compile-ignore-library-directory t
-  "If non-nil, ProofGeneral does not compile modules from the coq library.
-Should be `t' for normal coq users. If `nil' library modules are
-compiled if their sources are newer.
-
-This option has currently no effect, because Proof General uses
-coqdep to translate qualified identifiers into library file names
-and coqdep does not output dependencies in the standard library."
-  :type 'boolean
-  :safe 'booleanp
-  :group 'coq-auto-compile)
-
 (defcustom coq-coqdep-error-regexp
   (concat "^\\*\\*\\* Warning: in file .*, library .* is required "
           "and has not been found")
@@ -502,23 +506,14 @@ for instance, not make sense to let ProofGeneral check if the coq
 standard library is up-to-date. This function is always invoked
 on the .vo file name, regardless whether the file would be
 compiled with ``-quick'' or not."
-  (or
-   (and
-    coq-compile-ignore-library-directory
-    (eq (compare-strings coq-library-directory 0 nil
-                         lib-obj-file 0 (length coq-library-directory))
-        t)
-    (when coq--debug-auto-compilation
-      (message "Ignore lib file %s" lib-obj-file))
-    t)
-   (if (some
-          (lambda (dir-regexp) (string-match dir-regexp lib-obj-file))
-          coq-compile-ignored-directories)
-       (progn
-         (when coq--debug-auto-compilation
-	   (message "Ignore %s" lib-obj-file))
-         t)
-     nil)))
+  (if (some
+       (lambda (dir-regexp) (string-match dir-regexp lib-obj-file))
+       coq-compile-ignored-directories)
+      (progn
+	(when coq--debug-auto-compilation
+	  (message "Ignore %s" lib-obj-file))
+	t)
+    nil))
 
 ;;; convert .vo files to .v files and module names
 
@@ -544,7 +539,10 @@ Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix."
 
 (defun coq-unlock-ancestor (ancestor-src)
   "Unlock ANCESTOR-SRC."
-  (let* ((true-ancestor (file-truename ancestor-src)))
+  (let* ((default-directory
+	   (buffer-local-value 'default-directory
+			       (or proof-script-buffer (current-buffer))))
+	 (true-ancestor (file-truename ancestor-src)))
     (setq proof-included-files-list
           (delete true-ancestor proof-included-files-list))
     (proof-restart-buffers (proof-files-to-buffers (list true-ancestor)))))
@@ -561,11 +559,14 @@ Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix."
   "Display COMMAND and ERROR-MESSAGE in `coq--compile-response-buffer'.
 If needed, reinitialize `coq--compile-response-buffer'. Then
 display COMMAND and ERROR-MESSAGE."
-  (unless (buffer-live-p coq--compile-response-buffer)
+  (unless (buffer-live-p (get-buffer coq--compile-response-buffer))
     (coq-init-compile-response-buffer))
-  (let ((inhibit-read-only t))
+  (let ((inhibit-read-only t)
+	(deactivate-mark nil))
     (with-current-buffer coq--compile-response-buffer
-      (insert command "\n" error-message)))
+      (save-excursion
+	(goto-char (point-max))
+	(insert command "\n" error-message "\n"))))
   (when display
     (coq-display-compile-response-buffer)))
 
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 20440758..8901a008 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -85,12 +85,15 @@
 ;; back into proof-action-list only if all top-level jobs of those
 ;; modules that are required before it are finished.
 ;;
-;; A problem occurs with "Require b a.", where b depends on a. To
-;; avoid cycles in the dependency graph, here the top-level
-;; compilation job for "a" will be a so-called clone of the real
-;; compilation job. The Require item is stored with the clone. The
-;; real job has dependency links to all its clones. Every clone waits
-;; until its real job has finished.
+;; A problem occurs with "Require a. Require a.", where two different
+;; action list pieces must be stored with the job for a. The solution
+;; here is to clone the original job when it is needed more than one
+;; time. This cloning is done in general and not only for top-level
+;; jobs. So also when a.v and b.v both depend on c.v, the second
+;; dependency link is managed by a clone of the job for c.v. Every
+;; real job has dependency links to all its clones. All clones wait
+;; until the original job has finished. (In retrospect it seems a
+;; design without clone jobs might have been cleaner.)
 ;;
 ;; For 2- make sure ancestors are properly locked:
 ;;
@@ -101,27 +104,44 @@
 ;; when only "Require a." is retracted.
 ;;
 ;; The problem is solved with the 'coq-locked-ancestors property of
-;; spans that contain Require commands and with the
-;; coq--par-ancestor-files hash. Ancestors in the 'coq-locked-ancestors
-;; property are unlocked when this span is retracted. As locking is
-;; done eagerly (as soon as coqdep runs first on the file), I only
-;; have to make sure the right files appear in 'coq-locked-ancestors.
+;; spans that contain Require commands. Ancestors in the
+;; 'coq-locked-ancestors property are unlocked when this span is
+;; retracted. As locking is done eagerly (as soon as coqdep runs first
+;; on the file), I only have to make sure the right files appear in
+;; 'coq-locked-ancestors.
 ;;
-;; Ancestor files accumulate in compilation jobs when the compilation
-;; walks upwards the dependency tree. In the end, every top-level job
-;; contains a list of all its direct and indirect ancestors. Because
-;; of eager locking, all its ancestors are already locked, when a
-;; top-level job is about to be retired. The coq--par-ancestor-files
-;; hash therefore records whether some ancestor does already appear in
-;; the 'coq-locked-ancestors property of some span before the current
-;; one. If it doesn't, I store it in the current span.
+;; Ancestors accumulate in compilation jobs when the compilation walks
+;; upwards the dependency tree. In the end, every top-level job
+;; contains a list of all its direct and indirect ancestors in its
+;; 'ancestors property. Because of eager locking, all its ancestors
+;; are already locked, when a top-level job is about to be retired.
+;; Every job records in his 'locked propery whether the file
+;; corresponding to this job has been registered in some
+;; 'coq-locked-ancestors property already.
 ;;
 ;; For 3- error reporting:
 ;;
-;; For now, all compilation jobs are killed on the first error. All
-;; items that are not yet asserted are retract. This is done with
-;; signalling an error and calling `coq-par-emergency-cleanup' in the
-;; sentinel, if there was an error.
+;; Depending on `coq-compile-keep-going' compilation can continue
+;; after an error or stop immediately. For stopping immediately,
+;; processing is aborted with a signal that eventually leads to
+;; `coq-par-emergency-cleanup', which kills all compilation jobs,
+;; retracts the queue region and resets all internal data.
+;;
+;; For `coq-compile-keep-going', the failing job and all dependants
+;; are marked as 'failed. Queue dependants are marked with
+;; 'queue-failed. These marked jobs continue with their normal state
+;; transition, but omit certain steps (eg., running coqc). The first
+;; tricky part is how to unlock ancestors. When marking jobs as
+;; failed, their ancestors (and thereby also the files for the jobs
+;; themselves) are unlocked, unless they are still participating in an
+;; ongoing compilation. If a coqc compilation finishes and all
+;; dependants are marked as failed, ancestors are also unlocked in the
+;; same way. If a top-level job is marked as 'queue-failed, its
+;; ancestors are unlocked when this job finishes coqc compilation.
+;;
+;; The second tricky part is how to delete the queue region. For that
+;; the last top-level job is delayed until proof-action-list is empty.
+;; Then the whole queue is deleted.
 ;;
 ;; For 4- using -quick and the handling of .vo/.vio prerequisites
 ;;
@@ -185,13 +205,22 @@
 ;;   'src-file        - the .v file name
 ;;   'load-path       - value of coq-load-path, propagated to all
 ;;                      dependencies 
-;;   'ancestor-files  - list of ancestors, including the source file
-;;                      of this job
-;;   'require-span    - present for top-level jobs only, there it
+;;   'ancestors       - list of ancestor jobs, for real compilation jobs
+;;                      this list includes the job itself; may contain
+;;                      duplicates
+;;   'lock-state      - nil for clone jobs, 'unlocked if the file
+;;                      corresponding to job is not locked, 'locked if that
+;;                      file has been locked, 'asserted if it has been
+;;                      registered in some span in the 'coq-locked-ancestors
+;;                      property already
+;;   'require-span    - present precisely for top-level jobs only, there it
 ;;                      contains the span that must finally store the
 ;;                      ancestors
 ;;   'vio2vo-needed   - t if a subsequent vio2vo process is required to
 ;;                      build the .vo file. Otherwiese nil.
+;;   'failed          - t if coqdep or coqc for the job or one dependee failed.
+;;   'queue-failed    - t if some direct or indirect queue dependee is
+;;                      marked 'failed
 ;;   'visited         - used in the dependency cycle detection to mark
 ;;                      visited jobs
 ;;
@@ -244,16 +273,6 @@
 ;;                                the process is killed
 ;;
 ;;
-;; Symbols in the coq--par-ancestor-files hash
-;;
-;; This hash maps file names to symbols. A file is present in the
-;; hash, if it has been locked.
-;;
-;;   'locked   - the file is not yet stored in the
-;;               'coq-locked-ancestors property of some span
-;;   'asserted - the file has been stored in some span
-;;
-;;
 ;; To print the states of the compilation jobs for debugging, eval
 ;; 
 ;; (let ((clones))
@@ -283,22 +302,6 @@
 
 ;;; Variables
 
-(defvar coq--par-ancestor-files nil
-  "Hash remembering the state of locked ancestor files.
-This hash maps true file names (in the sense of `file-truename')
-to either 'locked or 'asserted.
-
-'locked means that this ancestor file has been locked
-already (because it appeared in the dependency tree somewhere and
-coqdep has been started on it) but has not been assigned to the
-'coq-locked-ancestors property of some span. That is, 'locked
-ancestors are not an ancestor of any required module in the
-asserted region.
-
-'asserted means that this ancestor is the ancestor of some
-asserted required module (and is in some 'coq-locked-ancestors
-property).")
-
 (defvar coq--current-background-jobs 0
   "Number of currently running background jobs.")
 
@@ -321,10 +324,25 @@ Used to link top-level jobs with queue dependencies.")
 (defvar coq--compile-vio2vo-delay-timer nil
   "Holds the timer for the vio2vo delay.")
 
+(defvar coq--compile-vio2vo-start-id 0
+  "Integer counter to detect races for `coq-par-require-processed'.
+Assume compilation for the last top-level ``Require'' command
+finishes but executing the ``Require'' takes so long that the
+user can assert a next ``Require'' and that the second
+compilation finishes before the first ``Require'' has been
+processed. In this case there are two `coq-par-require-processed'
+callbacks active, of which the first one must be ignored. For
+each new callback this counter is incremented and when there is a
+difference the call to `coq-par-require-processed' is ignored.")
+
 (defvar coq--par-next-id 1
   "Increased for every job and process, to get unique job names.
 The names are only used for debugging.")
 
+(defvar coq--par-delayed-last-job nil
+  "Inform the cycle detection that there is a delayed top-level job.
+If t, there is a delayed top-level job (for which the compilation failed).")
+
 
 ;;; utility functions
 
@@ -366,14 +384,6 @@ latter greater then everything else."
   "(Re-)Initialize `coq--compilation-object-hash'."
   (setq coq--compilation-object-hash (make-hash-table :test 'equal)))
 
-(defun coq-par-init-ancestor-hash ()
-  "(Re-)Initialize `coq--par-ancestor-files'"
-  (setq coq--par-ancestor-files (make-hash-table :test 'equal))
-  (mapc
-   (lambda (locked-anc)
-     (puthash locked-anc 'asserted coq--par-ancestor-files))
-   proof-included-files-list))
-
 ;;; generic queues
 ;; Standard implementation with two lists.
 
@@ -570,8 +580,8 @@ this buffer visible and returns a string.
 This function does always return .vo dependencies, regardless of the
 value of `coq-compile-quick'. If necessary, the conversion into .vio
 files must be done elsewhere."
-  (when coq--debug-auto-compilation
-    (message "analyse coqdep output \"%s\"" output))
+  ;; (when coq--debug-auto-compilation
+  ;;   (message "analyse coqdep output \"%s\"" output))
   (if (or
        (not (eq status 0))
        (string-match coq-coqdep-error-regexp output))
@@ -707,7 +717,8 @@ function returns () if MODULE-ID comes from the standard library."
 ;;; manage background jobs
 
 (defun coq-par-kill-all-processes ()
-  "Kill all background coqc, coqdep or vio2vo compilation processes."
+  "Kill all background coqc, coqdep or vio2vo compilation processes.
+Return t if some process was killed."
   ;; need to first mark processes as killed, because delete process
   ;; starts running sentinels in the order processes terminated, so
   ;; after the first delete-process we see sentinentels of non-killed
@@ -731,40 +742,48 @@ function returns () if MODULE-ID comes from the standard library."
 		    (get (process-get process 'coq-compilation-job) 'name)
 		    (process-name process)))))
      (process-list))
-    (setq coq--current-background-jobs 0)))
+    (setq coq--current-background-jobs 0)
+    kill-needed))
 
-(defun coq-par-unlock-ancestors-on-error ()
+(defun coq-par-unlock-all-ancestors-on-error ()
   "Unlock ancestors which are not in an asserted span.
 Used for unlocking ancestors on compilation errors."
-  (when coq--par-ancestor-files
-    ;; nil e.g. when enabling on-the-fly compilation after processing imports.
+  (when coq--compilation-object-hash
     (maphash
-     (lambda (ancestor state)
-       (when (eq state 'locked)
-         (coq-unlock-ancestor ancestor)
-         (puthash ancestor nil coq--par-ancestor-files)))
-     coq--par-ancestor-files)))
+     (lambda (key job)
+       (when (eq (get job 'lock-state) 'locked)
+         (coq-unlock-ancestor (get job 'src-file))
+	 (put job 'lock-state 'unlocked)))
+     coq--compilation-object-hash)))
 
 (defun coq-par-emergency-cleanup ()
   "Emergency cleanup for parallel background compilation.
 Kills all processes, unlocks ancestors, clears the queue region
 and resets the internal state."
-  (when coq--debug-auto-compilation
-    (message "emergency cleanup"))
-  (coq-par-kill-all-processes)
-  (setq coq-par-compilation-queue (coq-par-new-queue))
-  (setq coq--last-compilation-job nil)
-  (setq coq-par-vio2vo-queue (coq-par-new-queue))
-  (setq coq--compile-vio2vo-in-progress nil)
-  (when coq--compile-vio2vo-delay-timer
-    (cancel-timer coq--compile-vio2vo-delay-timer))
-  (when proof-action-list
-    (setq proof-shell-interrupt-pending t))
-  (coq-par-unlock-ancestors-on-error)
-  (proof-release-lock)
-  (proof-detach-queue)
-  (setq proof-second-action-list-active nil)
-  (coq-par-init-compilation-hash))
+  (interactive)				; needed for menu
+  (let (proc-killed was-busy)
+    (when coq--debug-auto-compilation
+      (message "emergency cleanup"))
+    (setq proc-killed (coq-par-kill-all-processes))
+    (when (and (boundp 'prover-was-busy)
+	       (or proc-killed coq--last-compilation-job
+		   coq--compile-vio2vo-in-progress
+		   coq--compile-vio2vo-delay-timer))
+      (setq prover-was-busy t))
+    (setq coq-par-compilation-queue (coq-par-new-queue))
+    (setq coq--last-compilation-job nil)
+    (setq coq-par-vio2vo-queue (coq-par-new-queue))
+    (setq coq--compile-vio2vo-in-progress nil)
+    (when coq--compile-vio2vo-delay-timer
+      (cancel-timer coq--compile-vio2vo-delay-timer)
+      (setq coq--compile-vio2vo-delay-timer nil))
+    (coq-par-unlock-all-ancestors-on-error)
+    (when proof-action-list
+      (setq proof-shell-interrupt-pending t))
+    (proof-release-lock)
+    (proof-detach-queue)
+    (setq proof-second-action-list-active nil)
+    (coq-par-init-compilation-hash)))
 
 (defun coq-par-process-filter (process output)
   "Store output from coq background compilation."
@@ -855,6 +874,7 @@ errors are reported with an error message."
 	    (setq coq--compile-vio2vo-in-progress nil)
 	    (message "vio2vo compilation finished"))
 	  (when (and
+		 (not coq--par-delayed-last-job)
 		 (eq coq--current-background-jobs 0)
 		 coq--last-compilation-job)
 	    (let ((cycle (coq-par-find-dependency-circle)))
@@ -891,15 +911,30 @@ errors are reported with an error message."
 		(length (cdr coq-par-vio2vo-queue)))))
   (coq-par-start-jobs-until-full))
 
-(defun coq-par-require-processed (span)
-  "Callback for `proof-action-list' to start vio2vo compilation.
-This callback is inserted with a dummy item after the last
-require command to start vio2vo compilation after
-`coq-compile-vio2vo-delay' seconds."
-  (assert (not coq--last-compilation-job)
-	  nil "normal compilation and vio2vo in parallel 1")
-  (setq coq--compile-vio2vo-delay-timer
-	(run-at-time coq-compile-vio2vo-delay nil 'coq-par-run-vio2vo-queue)))
+(defun coq-par-require-processed (race-counter)
+  "Callback for `proof-action-list' to signal completion of the last require.
+This function ensures that vio2vo compilation starts after
+`coq-compile-vio2vo-delay' seconds after the last module has been
+loaded into Coq. When background compilation is successful, this
+callback is inserted with a dummy item into proof-action-list
+somewhere after the last require command."
+  ;; When the user asserts new stuff while the (previously) last
+  ;; require command is being processed, `coq--last-compilation-job'
+  ;; might get non-nil. In this case there is a new last compilation
+  ;; job that will eventually trigger vio2vo compilation.
+  (unless (or coq--last-compilation-job
+	      (not (eq race-counter coq--compile-vio2vo-start-id)))
+    (setq coq--compile-vio2vo-delay-timer
+	  (run-at-time coq-compile-vio2vo-delay nil
+		       'coq-par-run-vio2vo-queue))))
+
+(defun coq-par-callback-queue-item (callback)
+  ;; A proof-action-list item has the form of
+  ;;            (SPAN COMMANDS ACTION [DISPLAYFLAGS])
+  ;; If COMMANDS is nil, the item is processed as comment and not sent
+  ;; to the proof assistant, only the callback is called, see
+  ;; proof-shell.el.
+  (list nil nil callback))
 
 
 ;;; background job tasks
@@ -1105,21 +1140,75 @@ therefore delete a file if it might be in the way. Sets the
 	 (signal 'coq-compile-error-rm err))))
     result))
 
+(defun coq-par-retire-top-level-job (job)
+  "Register ancestors and start queue items.
+This function performs the essential tasks for top-level jobs
+when they transition from 'waiting-queue to 'ready:
+- Registering ancestors in the span and recording this fact in
+  the 'lock-state property.
+- Moving queue items back to `proof-action-list' and start their
+  execution.
+- Insert `coq-par-require-processed' as callback if this is the
+  last top-level job, such that vio2vo compilation will start
+  eventually.
+
+This function can safely be called for non-top-level jobs. This
+function must not be called for failed jobs."
+  (assert (not (get job 'failed))
+	  nil "coq-par-retire-top-level-job precondition failed")
+  (let ((span (get job 'require-span))
+	(items (get job 'queueitems)))
+    (when (and span coq-lock-ancestors)
+      (dolist (anc-job (get job 'ancestors))
+	(assert (not (eq (get anc-job 'lock-state) 'unlocked))
+		nil "bad ancestor lock state")
+	(when (eq (get anc-job 'lock-state) 'locked)
+	  (put anc-job 'lock-state 'asserted)
+	  (push (get anc-job 'src-file)
+		(span-property span 'coq-locked-ancestors)))))
+    (when items
+      (when (and (eq coq-compile-quick 'quick-and-vio2vo)
+		 (eq coq--last-compilation-job job))
+	(let ((vio2vo-counter
+	       (setq coq--compile-vio2vo-start-id
+		     (1+ coq--compile-vio2vo-start-id))))
+	  ;; Insert a notification callback for when the last require
+	  ;; queue item has been processed.
+	  (setq items
+		(cons
+		 (car items)		; this is the require
+		 (cons
+		  (coq-par-callback-queue-item
+		   `(lambda (span) (coq-par-require-processed ,vio2vo-counter)))
+		  (cdr items))))))
+      (proof-add-to-queue items 'advancing)
+      (when coq--debug-auto-compilation
+	(message "%s: add %s items to action list"
+		 (get job 'name) (length items)))
+      (put job 'queueitems nil))))
+
 (defun coq-par-kickoff-queue-maybe (job)
   "Try transition 'waiting-queue -> 'ready for job JOB.
 This transition is only possible if JOB is in state
 'waiting-queue and if it has no queue dependee. If this is the
 case, the following actions are taken:
-- for top-level jobs (non-nil 'require-span property), ancestors
-  are registered in `coq--par-ancestor-files' and in the span in
-  'queue-span
-- processing of items in 'queueitems is started
+- for successful top-level jobs (non-nil 'require-span property), ancestors
+  are registered in the 'queue-span and marked as 'asserted in their
+  'lock-state property
+- processing of items in 'queueitems is started (if JOB is successful)
 - a possible queue dependant gets it's dependency cleared, and,
   if possible the 'waiting-queue -> 'ready transition
   is (recursively) done for the dependant
 - if this job is the last top-level compilation
   job (`coq--last-compilation-job') then the last compilation job
-  and `proof-second-action-list-active' are cleared."
+  and `proof-second-action-list-active' are cleared and vio2vo
+  processing is triggered.
+- If compilation failed, the (failing) last top-level job is
+  delayed until `proof-action-list' is empty, possibly by
+  registering this call as a callback in an empty
+  proof-action-list item. When proof-action-list is empty, the
+  queue span is deleted, remaining spans are cleared and the
+  `proof-shell-busy' lock is freed."
   (if (or (not (eq (get job 'state) 'waiting-queue))
 	  (get job 'queue-dependant-waiting))
       (when coq--debug-auto-compilation
@@ -1131,62 +1220,61 @@ case, the following actions are taken:
 	   (get job 'name))))
     (when coq--debug-auto-compilation
       (message "%s: has itself no queue dependency" (get job 'name)))
-    (when (and (get job 'require-span) coq-lock-ancestors)
-      (let ((span (get job 'require-span)))
-	(dolist (f (get job 'ancestor-files))
-	  (unless (eq (gethash f coq--par-ancestor-files) 'asserted)
-	    (puthash f 'asserted coq--par-ancestor-files)
-	    (span-set-property
-	     span 'coq-locked-ancestors
-	     (cons f (span-property span 'coq-locked-ancestors)))))))
-    (when (get job 'queueitems)
-      (let ((items (get job 'queueitems)))
-	(when (and (eq coq--last-compilation-job job)
-		   (eq coq-compile-quick 'quick-and-vio2vo))
-	  ;; Insert the vio2vo start notification callback after the
-	  ;; require item.
-	  (setq items
-		(cons
-		 (car items)
-		 (cons
-		  ;; A proof-action-list item is
-		  ;; (SPAN COMMANDS ACTION [DISPLAYFLAGS])
-		  ;; If COMMANDS is nil, the item is processed as
-		  ;; comment and not sent to the proof assistant, see
-		  ;; proof-shell.el.
-		  (list nil nil 'coq-par-require-processed)
-		  (cdr items)))))
-	(proof-add-to-queue items 'advancing)
-	(when coq--debug-auto-compilation
-	  (message "%s: add %s items to action list"
-		   (get job 'name) (length items)))
-	(put job 'queueitems nil)))
-    (put job 'state 'ready)
-    (when coq--debug-auto-compilation
-      (message "%s: ready" (get job 'name)))
-    (let ((dependant (get job 'queue-dependant)))
-      (if dependant
-	  (progn
-	    (assert (not (eq coq--last-compilation-job job))
-		    nil "coq--last-compilation-job invariant error")
-	    (put dependant 'queue-dependant-waiting nil)
-	    (when coq--debug-auto-compilation
-	      (message
-	       "%s -> %s: clear queue dependency, kickoff queue at %s"
-	       (get job 'name) (get dependant 'name) (get dependant 'name)))
-	    (coq-par-kickoff-queue-maybe dependant)
+    (unless (get job 'failed)
+      (coq-par-retire-top-level-job job))
+    (when (and (get job 'failed) (get job 'require-span))
+      (setq coq--par-delayed-last-job nil))
+    (if (and (get job 'failed)
+	     (eq coq--last-compilation-job job)
+	     proof-action-list)
+	(progn
+	  (when coq--debug-auto-compilation
+	    (message "%s: delay queue kickoff until action list is empty"
+		     (get job 'name)))
+	  (setq coq--par-delayed-last-job t)
+	  (proof-add-to-queue
+	   (list (coq-par-callback-queue-item
+		  `(lambda (span) (coq-par-kickoff-queue-maybe ',job))))
+	   'advancing))
+      (put job 'state 'ready)
+      (when coq--debug-auto-compilation
+	(message "%s: ready" (get job 'name)))
+      (let ((dependant (get job 'queue-dependant)))
+	(if dependant
+	    (progn
+	      (assert (not (eq coq--last-compilation-job job))
+		      nil "coq--last-compilation-job invariant error")
+	      (put dependant 'queue-dependant-waiting nil)
+	      (when coq--debug-auto-compilation
+		(message
+		 "%s -> %s: clear queue dependency, kickoff queue at %s"
+		 (get job 'name) (get dependant 'name) (get dependant 'name)))
+	      (coq-par-kickoff-queue-maybe dependant)
+	      (when coq--debug-auto-compilation
+		(message "%s: queue kickoff finished"
+			 (get job 'name))))
+	  (when (eq coq--last-compilation-job job)
+	    (when (get job 'failed)
+	      ;; proof-action-list is empty, see above
+	      ;; variables that hold the queue span are buffer local
+	      (with-current-buffer (or proof-script-buffer (current-buffer))
+		(proof-script-clear-queue-spans-on-error nil))
+	      (proof-release-lock)
+	      (when (eq coq-compile-quick 'quick-and-vio2vo)
+		(assert (not coq--compile-vio2vo-delay-timer)
+			nil "vio2vo timer set before last compilation job")
+		(setq coq--compile-vio2vo-delay-timer
+		      (run-at-time coq-compile-vio2vo-delay nil
+				   'coq-par-run-vio2vo-queue))))
+	    (setq coq--last-compilation-job nil)
+	    (setq proof-second-action-list-active nil)
 	    (when coq--debug-auto-compilation
-	      (message "%s: queue kickoff finished"
-		       (get job 'name))))
-	(when (eq coq--last-compilation-job job)
-	  (setq coq--last-compilation-job nil)
-	  (setq proof-second-action-list-active nil)
+	      (message "clear last compilation job"))
+	    (message "Library compilation %s"
+		     (if (get job 'failed) "failed" "finished successfully")))
 	  (when coq--debug-auto-compilation
-	    (message "clear last compilation job"))
-	  (message "Library compilation finished"))
-	(when coq--debug-auto-compilation
-	  (message "%s: no queue dependant, queue kickoff finished"
-		   (get job 'name)))))))
+	    (message "%s: no queue dependant, queue kickoff finished"
+		     (get job 'name))))))))
 
 (defun coq-par-compile-job-maybe (job)
   "Choose next action for JOB after dependencies are ready.
@@ -1199,19 +1287,21 @@ JOB stays in 'enqueued-coqc for the time being. Otherwise, the
 transition 'enqueued-coqc -> 'waiting-queue is done and, if
 possible, also 'waiting-queue -> 'ready."
   (put job 'state 'enqueued-coqc)
-  ;; note that coq-par-job-needs-compilation sets 'required-obj-file
+  ;; Note that coq-par-job-needs-compilation sets 'required-obj-file
   ;; as a side effect and deletes .vo or .vio files that are in the way.
-  ;; It also puts job into the vio2vo queue, if necessary.
-  (if (coq-par-job-needs-compilation job)
+  ;; It also sets the 'vio2vo-needed property if needed.
+  (if (and (not (get job 'failed)) (coq-par-job-needs-compilation job))
       (coq-par-start-or-enqueue job)
     (when coq--debug-auto-compilation
-      (message "%s: up-to-date, no compilation" (get job 'name)))
+      (message "%s: %s, no compilation"
+	       (get job 'name)
+	       (if (get job 'failed) "failed" "up-to-date")))
     (when (get job 'vio2vo-needed)
       (coq-par-vio2vo-enqueue job))
     (coq-par-kickoff-coqc-dependants job (get job 'youngest-coqc-dependency))))
 
 (defun coq-par-decrease-coqc-dependency (dependant dependee-time
-						   dependee-ancestor-files)
+						   dependee-ancestors)
   "Clear Coq dependency and update dependee information in DEPENDANT.
 This function handles a Coq dependency from child dependee to
 parent dependant when the dependee has finished compilation (ie.
@@ -1229,8 +1319,8 @@ For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for
   (when (coq-par-time-less (get dependant 'youngest-coqc-dependency)
 			   dependee-time)
     (put dependant 'youngest-coqc-dependency dependee-time))
-  (put dependant 'ancestor-files
-       (append dependee-ancestor-files (get dependant 'ancestor-files)))
+  (put dependant 'ancestors
+       (append dependee-ancestors (get dependant 'ancestors)))
   (put dependant 'coqc-dependency-count
        (1- (get dependant 'coqc-dependency-count)))
   (assert (<= 0 (get dependant 'coqc-dependency-count))
@@ -1258,7 +1348,8 @@ waiting-queue for JOB.
 
 DEP-TIME is either 'just-compiled, when JOB has just finished
 compilation, or the most recent modification time of all
-dependencies of JOB.
+dependencies of JOB. (If compilation for JOB failed, DEP-TIME is
+meaningless but should nevertheless be a non-nil valid argument.)
 
 This function makes the following actions.
 - Clear the dependency from JOB to all its dependants, thereby
@@ -1267,16 +1358,22 @@ This function makes the following actions.
 - save the maximum of DEP-TIME and .vo modification time in
   'youngest-coqc-dependency, in case we later create a clone of this job
 - put JOB into state 'waiting-queue
-- try to trigger the transition 'waiting-queue -> ready for JOB"
-  (let ((ancestor-files (get job 'ancestor-files)))
+- try to trigger the transition 'waiting-queue -> ready for JOB
+- If JOB is successful but all dependants have failed, unlock all
+  ancestors in case they are not participating in a still ongoing
+  compilation."
+  (let ((ancestors (get job 'ancestors))
+	(dependant-alive nil))
+    (put job 'state 'waiting-queue)
     ;; take max of dep-time and obj-mod-time
     ;; 
     ;; dep-time is either 'just-compiled or 'youngest-coqc-dependency of
     ;; the dependee, in the latter case obj-mod-time is greater than
     ;; dep-time, because otherwise we would have compiled the file. For
     ;; a clone job the max has already been taken when processing the
-    ;; original file.
-    (unless (or (eq dep-time 'just-compiled) (eq (get job 'type) 'clone))
+    ;; original file. If coqdep failed, 'obj-mod-time is not set.
+    (unless (or (eq dep-time 'just-compiled) (eq (get job 'type) 'clone)
+		(get job 'failed))
       (setq dep-time (get job 'obj-mod-time)))
     (put job 'youngest-coqc-dependency dep-time)
     (when coq--debug-auto-compilation
@@ -1285,33 +1382,45 @@ This function makes the following actions.
 	       (if (eq dep-time 'just-compiled)
 		   'just-compiled
 		 (current-time-string dep-time))))
-    (put job 'state 'waiting-queue)
-    (mapc
-     (lambda (dependant)
-       (coq-par-decrease-coqc-dependency dependant dep-time ancestor-files))
-     (get job 'coqc-dependants))
+    (dolist (dependant (get job 'coqc-dependants))
+      (coq-par-decrease-coqc-dependency dependant dep-time ancestors)
+      (unless (get dependant 'failed)
+	(setq dependant-alive t)))
     (when coq--debug-auto-compilation
-      (message "%s: coqc kickoff finished, maybe kickoff queue"
-	       (get job 'name)))
+      (message (concat "%s: coqc kickoff finished, %s dependant alive, "
+		       "maybe kickoff queue")
+	       (get job 'name)
+	       (if dependant-alive "some" "no")))
+    (assert (or (not (get job 'failed)) (not dependant-alive))
+	    nil "failed job with non-failing dependant")
+    (when (or (and (not dependant-alive)
+		   (not (get job 'require-span))
+		   (not (get job 'failed)))
+	      (and (get job 'queue-failed) (not (get job 'failed))))
+      ;; job has not failed, but all dependants have 'failed set, or
+      ;; top-level job marked with 'queue-failed changes to 'failed
+      (when (get job 'queue-failed)
+	(when coq--debug-auto-compilation
+	  (message "%s: queue-failed -> failed, unlock ancestors"
+		   (get job 'name)))
+	(put job 'failed t))
+      (coq-par-unlock-job-ancestors-on-error job))
     (coq-par-kickoff-queue-maybe job)))
 
 (defun coq-par-start-coqdep (job)
   "Start coqdep for JOB.
-Besides starting the background process, the source file is
-locked, registered in the 'ancestor-files property of JOB and in
-`coq--par-ancestor-files'"
-  (let ((true-src (file-truename (get job 'src-file))))
-    (when coq-lock-ancestors
-      (proof-register-possibly-new-processed-file true-src)
-      (put job 'ancestor-files (list true-src))
-      (unless (gethash true-src coq--par-ancestor-files)
-	(puthash true-src 'locked coq--par-ancestor-files)))
-    (coq-par-start-process
-     coq-dependency-analyzer
-     (coq-par-coqdep-arguments (get job 'src-file) (get job 'load-path))
-     'coq-par-process-coqdep-result
-     job
-     nil)))
+Lock the source file and start the coqdep background process"
+  (when (and coq-lock-ancestors
+	     (eq (get job 'lock-state) 'unlocked))
+    (proof-register-possibly-new-processed-file (get job 'src-file))
+    (push job (get job 'ancestors))
+    (put job 'lock-state 'locked))
+  (coq-par-start-process
+   coq-dependency-analyzer
+   (coq-par-coqdep-arguments (get job 'src-file) (get job 'load-path))
+   'coq-par-process-coqdep-result
+   job
+   nil))
 
 (defun coq-par-start-vio2vo (job)
   "Start vio2vo background job."
@@ -1431,7 +1540,7 @@ This function returns the newly created job."
 		  (put new-job 'state 'ready))
 		(put new-job 'youngest-coqc-dependency
 		     (get orig-job 'youngest-coqc-dependency))
-		(put new-job 'ancestor-files (get orig-job 'ancestor-files)))
+		(put new-job 'ancestors (get orig-job 'ancestors)))
 	    (coq-par-add-coqc-dependency orig-job new-job)
 	    (put new-job 'state 'waiting-dep)
 	    (put new-job 'youngest-coqc-dependency '(0 0))))
@@ -1443,32 +1552,131 @@ This function returns the newly created job."
 		   (buffer-file-name proof-script-buffer))
 	(signal 'coq-compile-error-circular-dep
 		(concat dependant " -> scripting buffer")))
-      (message "Check %s" (get new-job 'src-file))
       (put new-job 'load-path coq-load-path)
       (put new-job 'youngest-coqc-dependency '(0 0))
       (puthash module-vo-file new-job coq--compilation-object-hash)
       (when coq--debug-auto-compilation
 	(message "%s: create %s compilation for %s"
 		 (get new-job 'name) (get new-job 'type) module-vo-file))
+      (if (member (file-truename (get new-job 'src-file))
+		  proof-included-files-list)
+	  (put new-job 'lock-state 'asserted)
+	(put new-job 'lock-state 'unlocked))
       (when queue-dep
 	(coq-par-add-queue-dependency queue-dep new-job))
+      (message "Check %s" (get new-job 'src-file))
       (coq-par-start-or-enqueue new-job))
     new-job))
 
+(defun coq-par-ongoing-compilation (job)
+  "Determine if the source file for JOB needs to stay looked.
+Return t if job has a direct or indirect dependant that has not
+failed yet and that is in a state before 'waiting-queue. Also,
+return t if JOB has a dependant that is a top-level job which has
+not yet failed."
+  (assert (not (eq (get job 'lock-state) 'asserted))
+	  nil "coq-par-ongoing-compilation precondition failed")
+  (cond
+   ((get job 'failed)
+    nil)
+   ((or (eq (get job 'state) 'waiting-dep)
+	(eq (get job 'state) 'enqueued-coqc)
+	;; top-level job that has compilation finished but has not
+	;; been asserted yet
+	(and (eq (get job 'state) 'waiting-queue) (get job 'require-span))
+	;; Note that job cannot be a top-level in state 'ready,
+	;; because we started from job with 'lock-state property equal
+	;; to 'locked. Top-level job in state 'ready have all
+	;; dependees with 'lock-state equal to 'asserted.
+	)
+    t)
+   ;; Note that non-top-level jobs switch to 'waiting-queue as soon as
+   ;; all dependencies are ready, before they start to deal with the
+   ;; ancestors. We might therefore see here non-top-level jobs in
+   ;; state 'waiting-queue: they have successfully finished their
+   ;; compilation and are about to go to state 'ready.
+   ((or (eq (get job 'state) 'ready)
+	(eq (get job 'state) 'waiting-queue))
+    ;; internal ready job
+    (let ((dependants (get job 'coqc-dependants))
+	  (res nil)
+	  dep)
+      (while (and (not res) (setq dep (pop dependants)))
+	(setq res (coq-par-ongoing-compilation dep)))
+      res))
+   (t
+    (assert nil nil
+	    "impossible ancestor state %s on job %s"
+	    (get job 'state) (get job 'name)))))
+
+(defun coq-par-unlock-job-ancestors-on-error (job)
+  "Unlock those ancestors of JOB that need to be unlocked.
+For a failing job JOB, an ancestor need to stay looked if there
+is still some compilation going on for which this ancestor is a
+dependee or if a top level job with JOB as ancestor has finished
+it's compilation successfully. In all other cases the ancestor
+must be unlocked."
+  (dolist (anc-job (get job 'ancestors))
+    (when (and (eq (get anc-job 'lock-state) 'locked)
+	       (not (coq-par-ongoing-compilation anc-job)))
+      (when coq--debug-auto-compilation
+	(message "%s: %s unlock because no ongoing compilation"
+		 (get anc-job 'name) (get anc-job 'src-file)))
+      (coq-unlock-ancestor (get anc-job 'src-file))
+      (put anc-job 'lock-state 'unlocked))))
+
+(defun coq-par-mark-queue-failing (job)
+  "Mark JOB with 'queue-failed.
+Mark JOB with 'queue-failed, and, if JOB is in state
+'waiting-queue, transition to 'failed and unlock ancestors as
+appropriate."
+  (unless (or (get job 'failed) (get job 'queue-failed))
+    (put job 'queue-failed t)
+    (assert (not (eq (get job 'state) 'ready))
+	    nil "coq-par-mark-queue-failing impossible state")
+    (when coq--debug-auto-compilation
+      (message "%s: mark as queue-failed, %s"
+	       (get job 'name)
+	       (if (eq (get job 'state) 'waiting-queue)
+		   "failed, and unlock ancestors"
+		 "wait")))
+    (when (eq (get job 'state) 'waiting-queue)
+      (put job 'failed t)
+      (coq-par-unlock-job-ancestors-on-error job))
+    (when (get job 'queue-dependant)
+      (coq-par-mark-queue-failing (get job 'queue-dependant)))))
+
+(defun coq-par-mark-job-failing (job)
+  "Mark all dependants of JOB as failing and unlock ancestors as appropriate.
+Set the 'failed property on all direct and indirect dependants of
+JOB. Along the way, unlock ancestors as determined by
+`coq-par-ongoing-compilation'. Mark queue dependants with
+'queue-failed."
+  (unless (get job 'failed)
+    (put job 'failed t)
+    (when coq--debug-auto-compilation
+      (message "%s: mark as failed and unlock free ancestors" (get job 'name)))
+    (coq-par-unlock-job-ancestors-on-error job)
+    (dolist (dependant (get job 'coqc-dependants))
+      (coq-par-mark-job-failing dependant))
+    (when (get job 'queue-dependant)
+      (coq-par-mark-queue-failing (get job 'queue-dependant)))))
+
 (defun coq-par-process-coqdep-result (process exit-status)
   "Coqdep continuation function: Process coqdep output.
-This function analyses the coqdep output of PROCESS and signals
-an error if necessary. If there was no coqdep error, the
-following actions are taken.
+This function analyses the coqdep output of PROCESS. In case of
+error, the job is marked as failed or compilation is aborted via
+a signal (depending on `coq-compile-keep-going'). If there was no
+coqdep error, the following actions are taken.
 - the job that started PROCESS is put into sate 'waiting-dep
 - a new job is created for every dependency. If this new job is
   not immediately ready, a Coq dependency is registered from the
   new job to the current job. For dependencies that are 'ready
   already, the most recent ancestor modification time is
   propagated.
-- if there are no dependencies or all dependencies are ready
-  already, the next transition to 'enqueued-coqc is triggered for
-  the current job
+- if there are no dependencies (especially if coqdep failed) or
+  all dependencies are ready already, the next transition to
+  'enqueued-coqc is triggered for the current job
 - otherwise the current job is left alone until somebody
   decreases its dependency count to 0
 
@@ -1482,55 +1690,65 @@ is directly passed to `coq-par-analyse-coq-dep-exit'."
 	  (process-get process 'coq-process-command)))
 	job-max-time)
     (if (stringp dependencies-or-error)
-	(signal 'coq-compile-error-coqdep (get job 'src-file))
+	(if coq-compile-keep-going
+	    (coq-par-mark-job-failing job)
+	  (signal 'coq-compile-error-coqdep (get job 'src-file)))
 
       ;; no coqdep error -- work on dependencies
       (when coq--debug-auto-compilation
 	(message "%s: dependencies of %s are %s"
 		 (get job 'name) (get job 'src-file) dependencies-or-error))
-      (put job 'state 'waiting-dep)
       (setq job-max-time (get job 'youngest-coqc-dependency))
-      (mapc
-       (lambda (dep-vo-file)
-	 (unless (coq-compile-ignore-file dep-vo-file)
-	   (let* ((dep-job (coq-par-create-library-job dep-vo-file
-						       (get job 'load-path)
-						       nil nil
-						       (get job 'src-file)))
-		  (dep-time (get dep-job 'youngest-coqc-dependency)))
-	     (when (coq-par-time-less job-max-time dep-time)
-	       (setq job-max-time dep-time))
-	     (unless (coq-par-job-coqc-finished dep-job)
-	       (coq-par-add-coqc-dependency dep-job job)))))
-       dependencies-or-error)
-      (put job 'youngest-coqc-dependency job-max-time)
-      (if (coq-par-dependencies-ready job)
-	  (progn
-	    (when coq--debug-auto-compilation
-	      (message "%s: coqc dependencies finished" (get job 'name)))
-	    (coq-par-compile-job-maybe job))
-	(when coq--debug-auto-compilation
-	  (message "%s: wait for %d dependencies"
-		   (get job 'name) (get job 'coqc-dependency-count)))))))
+      (dolist (dep-vo-file dependencies-or-error)
+	(unless (coq-compile-ignore-file dep-vo-file)
+	  (let* ((dep-job (coq-par-create-library-job dep-vo-file
+						      (get job 'load-path)
+						      nil nil
+						      (get job 'src-file)))
+		 (dep-time (get dep-job 'youngest-coqc-dependency)))
+	    (when (coq-par-time-less job-max-time dep-time)
+	      (setq job-max-time dep-time))
+	    (unless (coq-par-job-coqc-finished dep-job)
+	      (coq-par-add-coqc-dependency dep-job job)))))
+      (put job 'youngest-coqc-dependency job-max-time))
+    ;; common part for job where coqdep was successful and where
+    ;; coqdep failed (when coq-compile-keep-going)
+    (put job 'state 'waiting-dep)
+    (if (coq-par-dependencies-ready job)
+	(progn
+	  (when coq--debug-auto-compilation
+	    (message "%s: coqc dependencies finished" (get job 'name)))
+	  (coq-par-compile-job-maybe job))
+      (when coq--debug-auto-compilation
+	(message "%s: wait for %d dependencies"
+		 (get job 'name) (get job 'coqc-dependency-count))))))
 
 (defun coq-par-coqc-continuation (process exit-status)
   "Coqc continuation function.
-Signal an error, if coqc failed. Otherwise, trigger the
-transition 'enqueued-coqc -> 'waiting-queue for the job behind
-PROCESS."
-  (if (eq exit-status 0)
-      (let ((job (process-get process 'coq-compilation-job)))
-	;; coqc success
-	(when (get job 'vio2vo-needed)
-	  (coq-par-vio2vo-enqueue job))
-	(coq-par-kickoff-coqc-dependants job 'just-compiled))
-    ;; coqc error
-    (coq-compile-display-error
-     (mapconcat 'identity (process-get process 'coq-process-command) " ")
-     (process-get process 'coq-process-output)
-     t)
-    (signal 'coq-compile-error-coqc
-	    (get (process-get process 'coq-compilation-job) 'src-file))))
+If coqc failed, signal an error or mark the job as 'failed, and
+unlock ancestors as appropriate. If coqc was successful, trigger
+the transition 'enqueued-coqc -> 'waiting-queue for the job
+behind PROCESS."
+  (let ((job (process-get process 'coq-compilation-job)))
+    (if (eq exit-status 0)
+	(progn
+	  ;; coqc success
+	  (when (get job 'vio2vo-needed)
+	    (coq-par-vio2vo-enqueue job))
+	  (coq-par-kickoff-coqc-dependants job 'just-compiled))
+      ;; coqc error
+      (coq-compile-display-error
+       (mapconcat 'identity (process-get process 'coq-process-command) " ")
+       (process-get process 'coq-process-output)
+       t)
+      (if coq-compile-keep-going
+	  (progn
+	    (coq-par-mark-job-failing job)
+	    (coq-par-kickoff-coqc-dependants
+	     job
+	     (get job 'youngest-coqc-dependency)))
+	(signal 'coq-compile-error-coqc
+		(get (process-get process 'coq-compilation-job) 'src-file))))))
 
 (defun coq-par-vio2vo-continuation (process exit-status)
   "vio2vo continuation function."
@@ -1688,7 +1906,6 @@ the maximal number of background compilation jobs is started."
 	     (length queueitems)))
   (unless coq--last-compilation-job
     (coq-par-init-compilation-hash)
-    (coq-par-init-ancestor-hash)
     (coq-init-compile-response-buffer))
   (let ((splitted-items
 	 (split-list-at-predicate queueitems
@@ -1711,7 +1928,8 @@ the maximal number of background compilation jobs is started."
     ;; notification
     (when (cdr splitted-items)
       (when coq--compile-vio2vo-delay-timer
-	(cancel-timer coq--compile-vio2vo-delay-timer))
+	(cancel-timer coq--compile-vio2vo-delay-timer)
+	(setq coq--compile-vio2vo-delay-timer nil))
       (when coq--compile-vio2vo-in-progress
 	(assert (not coq--last-compilation-job)
 		nil "normal compilation and vio2vo in parallel 2")
@@ -1720,9 +1938,8 @@ the maximal number of background compilation jobs is started."
 	(setq coq--compile-vio2vo-in-progress nil))
       ;; save buffers before invoking the first coqdep
       (coq-compile-save-some-buffers)
-      (mapc (lambda (require-items)
-	      (coq-par-handle-require-list require-items))
-	    (cdr splitted-items)))
+      (dolist (require-items (cdr splitted-items))
+	(coq-par-handle-require-list require-items)))
     (when coq--last-compilation-job
       (setq proof-second-action-list-active t))
     (coq-par-start-jobs-until-full)
@@ -1752,6 +1969,9 @@ does the error checking/reporting for
 		    "Proof General; please customize coq-pinned-version"))
 	 (message "%s \"%s\"; consider customizing coq-pinned-version"
 		  (get (car err) 'error-message) (cdr err))))
+      (file-error
+       (coq-par-emergency-cleanup)
+       (message "Error: %s" (mapconcat 'identity (cdr err) ": ")))
       (error
        (message "unexpected error during parallel compilation: %s"
 		err)
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 38ca5fd1..1c0b9c67 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -318,7 +318,7 @@ force indentation."
 The point should be at the beginning of the command name."
   (save-excursion ; FIXME Is there other module starting commands?
     (cond
-     ((looking-back "with\\s-+") "module") ; lowecase means Module that is not a declaration keyword (like in with Module) 
+     ((looking-back "with\\s-+" nil) "module") ; lowecase means Module that is not a declaration keyword (like in with Module) 
      ((proof-looking-at "\\(Module\\|Section\\)\\>")
       (if (coq-lonely-:=-in-this-command) "Module start" "Module def")))))
 
@@ -459,7 +459,7 @@ The point should be at the beginning of the command name."
      ((member corresp '("Inductive" "CoInductive")) ":= inductive")
      ((equal corresp "let") ":= let")
      ((equal corresp "where") ":= inductive") ;; inductive or fixpoint, nevermind
-     ((or (looking-back "{")) ":= record")
+     ((or (looking-back "{" nil)) ":= record")
      (t ":=")))) ; a parenthesis stopped the search
 
 
@@ -488,8 +488,8 @@ The point should be at the beginning of the command name."
 	  (cond
 	   ((member backtok '("." "Ltac")) "; tactic")
 	   ((equal backtok nil)
-	    (if (or (looking-back "(") (looking-back "\\[")
-		    (and (looking-back "{")
+	    (if (or (looking-back "(" nil) (looking-back "\\[")
+		    (and (looking-back "{" nil)
 			 (equal (coq-smie-backward-token) "{ subproof"))) ;; recursive call
 		"; tactic"
 	      "; record"))))))
@@ -505,10 +505,10 @@ The point should be at the beginning of the command name."
 		 (equal (coq-smie-backward-token) "; tactic")) ;; recursive
 	    "|| tactic")
 	   ;; this is wrong half of the time but should not harm indentation
-	   ((and (equal backtok nil) (looking-back "(")) "||") 
+	   ((and (equal backtok nil) (looking-back "(" nil)) "||") 
 	   ((equal backtok nil)
-	    (if (or (looking-back "\\[")
-		    (and (looking-back "{")
+	    (if (or (looking-back "\\[" nil)
+		    (and (looking-back "{" nil)
 			 (equal (coq-smie-backward-token) "{ subproof"))) ;; recursive call
 		"|| tactic"
 	      "||"))))))
@@ -549,7 +549,7 @@ The point should be at the beginning of the command name."
       (forward-char -1)
       (if (looking-at "{") "{ subproof" "} subproof"))
 
-     ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)"))
+     ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)" nil))
       ": ltacconstr")
 
      ((equal tok ":=")
diff --git a/coq/coq-system.el b/coq/coq-system.el
index 48757be5..88ce06be 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -57,10 +57,12 @@ See also `coq-prog-env' to adjust the environment."
   :group 'coq)
 
 (defun get-coq-library-directory ()
-  (let ((c (substring (shell-command-to-string (concat coq-prog-name " -where")) 0 -1 )))
-    (if (string-match "not found" c)
-        "/usr/local/lib/coq"
-      c)))
+  (let ((default-directory
+	  (if (file-accessible-directory-p default-directory)
+	      default-directory
+	    "/")))
+    (or (ignore-errors (car (process-lines coq-prog-name "-where")))
+	"/usr/local/lib/coq")))
 
 (defconst coq-library-directory (get-coq-library-directory) ;; FIXME Should be refreshed more often
   "The coq library directory, as reported by \"coqtop -where\".")
@@ -123,7 +125,11 @@ Interactively (with INTERACTIVE-P), show that number."
     ;; Use `shell-command' via `find-file-name-handler' instead of
     ;; `process-line': when the buffer is running TRAMP, PG uses
     ;; `start-file-process', loading the binary from the remote server.
-    (let* ((coq-command (shell-quote-argument (or coq-prog-name "coqtop")))
+    (let* ((default-directory
+	     (if (file-accessible-directory-p default-directory)
+		 default-directory
+	       "/"))
+	   (coq-command (shell-quote-argument (or coq-prog-name "coqtop")))
            (shell-command-str (format "%s -v" coq-command))
            (fh (find-file-name-handler default-directory 'shell-command))
            (retv (if fh (funcall fh 'shell-command shell-command-str (current-buffer))
diff --git a/coq/coq.el b/coq/coq.el
index 87641e57..e3541b48 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1354,6 +1354,8 @@ goal is redisplayed."
 (proof-definvisible coq-unset-printing-synth "Unset Printing Synth.")
 (proof-definvisible coq-set-printing-coercions "Set Printing Coercions.")
 (proof-definvisible coq-unset-printing-coercions "Unset Printing Coercions.")
+(proof-definvisible coq-set-printing-universes "Set Printing Universes.")
+(proof-definvisible coq-unset-printing-universes "Unset Printing Universes.")
 (proof-definvisible coq-set-printing-wildcards "Set Printing Wildcard.")
 (proof-definvisible coq-unset-printing-wildcards "Unset Printing Wildcard.")
 ; Takes an argument
@@ -1433,7 +1435,7 @@ Near here means PT is either inside or just aside of a comment."
     (cond
      ((coq-looking-at-comment)
       (coq-get-comment-region (point)))
-     ((and (looking-back proof-script-comment-end)
+     ((and (looking-back proof-script-comment-end nil)
            (save-excursion (forward-char -1) (coq-looking-at-comment)))
       (coq-get-comment-region (- (point) 1)))
      ((and (looking-at proof-script-comment-start)
@@ -1786,7 +1788,7 @@ Near here means PT is either inside or just aside of a comment."
 (defpacustom search-blacklist coq-search-blacklist-string
   "Strings to blacklist in requests to coq environment."
   :type 'string
-  ;;:get coq-search-blacklist-string
+  :get 'coq-get-search-blacklist
   :setting coq-set-search-blacklist)
 
 
@@ -1869,7 +1871,7 @@ The not yet delayed output is in the region
                 coq-proof-tree-additional-subgoal-ID-regexp end t)
           (let ((subgoal-id (match-string-no-properties 1)))
             (unless (gethash subgoal-id proof-tree-sequent-hash)
-              (message "CPTGNS new sequent %s found" subgoal-id)
+              ;; (message "CPTGNS new sequent %s found" subgoal-id)
               (setq proof-action-list
                     (cons (proof-shell-action-list-item
                            (coq-show-sequent-command subgoal-id)
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 748cf3ac..442ce6d5 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -920,7 +920,7 @@ example in Isabelle with semi-colons, but these will not appear in the
 final text.
 
 Coq, on the other hand, requires a full-stop terminator at the end of
-each line, so @kbd{C-c C-.} is the key binding used to turn on
+each line, so @kbd{C-c .} is the key binding used to turn on
 electric terminator.  If you don't know what the terminator character
 is, you can find the option anyway on the menu:
 @code{Proof-General -> Quick Options -> Processing -> Electric Terminator}
@@ -4396,12 +4396,19 @@ one project you can set the option as local file variable,
 @ref{Using file variables}. This can be done either directly in
 every file or once for all files of a directory tree with a
 @code{.dir-local.el} file, @inforef{Directory Variables, ,emacs}.
-For this case, this file should contain
+The file @code{.dir-local.el} should then contain
 
 @lisp
 ((coq-mode . ((coq-project-filename . "myprojectfile"))))
 @end lisp
 
+Note that variables set in @code{.dir-local.el} are automatically
+made buffer local (such that files in different directories can
+have their independent setting of @code{coq-project-filename}).
+If you make complex customizations using @code{eval} in
+@code{.dir-local.el}, you might want to add appropriate calls to
+@code{make-local-variable}.
+
 Documentation of the user option @code{coq-project-filename}:
 
 @c TEXI DOCSTRING MAGIC: coq-project-filename
@@ -4494,8 +4501,12 @@ these points:
 
 @itemize @bullet
 @item
-The option @code{coq-compile-before-require} must be
-turned on (menu @code{Coq -> Auto Compilation -> Compile Before Require}).
+Set the option @code{coq-compile-before-require} (menu @code{Coq
+-> Auto Compilation -> Compile Before Require}) to enable
+compilation before processing @code{Require} commands and set
+@code{coq-compile-parallel-in-background} (menu @code{Coq
+-> Auto Compilation -> Parallel background compilation}) for
+parallel asynchronous compilation (recommended).
 @item 
 Nonstandard load path elements @emph{must} be configured via a
 Coq project file (this is the recommended option),
@@ -4505,9 +4516,18 @@ option @code{coq-load-path}. @code{-I} or @code{-R} options in
 @item
 Configure
 @code{coq-max-background-compilation-jobs} if you want to limit
-the number of parallel background jobs.
+the number of parallel background jobs and set
+@code{coq-compile-keep-going} (menu @code{Coq -> Auto Compilation
+-> Keep going}) to let compilation continue after the first
+error.
 @end itemize
 
+To abort parallel background compilation, use @code{C-c C-c}
+(@code{proof-interrupt-process}), the tool bar interrupt icon,
+the menu entry @code{Abort Background Compilation} (menu
+@code{Coq -> Auto Compilation}) or kill the Coq toplevel via
+@code{C-c C-x} (@code{proof-shell-exit}). To abort synchronous
+single threaded compilation, simply hit @code{C-g}.
 
 
 @menu
@@ -4554,7 +4574,16 @@ controls how @code{-quick} and @code{.vio} files are used,
 @ref{Quick compilation and .vio Files}. This can also be
 configured in the menu @code{Coq -> Auto Compilation}.
 
-When a @code{Require} command causes a compilation of some files
+Similar to @code{make -k}, background compilation can be
+configured to continue as far as possible after the first error,
+see option @code{coq-compile-keep-going} (menu @code{Coq -> Auto
+Compilation -> Keep going}). The keep-going option only applies
+to errors from @code{coqdep} and @code{coqc}. For all other
+errors (for instance when the translation from logical module
+names to physical files fails or when starting @code{coqc} or
+@code{coqdep} fails), the compilation is immediately aborted.
+
+When a @code{Require} command causes a compilation of some files,
 one may wish to save some buffers to disk beforehand. The option
 @code{coq-compile-auto-save} controls how and which files are
 saved. There are two orthogonal choices: One may wish to save all
@@ -4583,8 +4612,11 @@ runs up to @code{coq-max-background-compilation-jobs} coqdep and
 coqc jobs in parallel in asynchronous subprocesses (or uses all
 your CPU cores if @code{coq-max-background-compilation-jobs}
 equals @code{'all-cpus}). Your Emacs will stay responsive during
-compilation. Use @code{C-c C-c} or the tool bar icons for
-interrupt or restart to interrupt compilation.
+compilation. To abort the background compilation process, use
+@code{C-c C-c} (@code{proof-interrupt-process}), the tool bar
+interrupt icon, the menu entry @code{Abort Background
+Compilation} (menu @code{Coq -> Auto Compilation}) or kill the
+Coq toplevel via @code{C-c C-x} (@code{proof-shell-exit}).
 
 For the usual case, you have at most
 `coq-max-background-compilation-jobs' parallel processes
@@ -4723,12 +4755,14 @@ files, but don't compile prerequisites for which an up-to-date
 @item quick-and-vio2vo
 Same as @code{quick-no-vio2vo}, but start vio2vo processes for
 missing @code{.vo} files after a certain delay when library
-complication for the current queue region has finished. With this
+compilation for the current queue region has finished. With this
 mode you might see asynchronous errors from vio2vo compilation
 while you are processing stuff far below the last require. vio2vo
 compilation is done on a subset of the available cores controlled
 by option @code{coq-compile-vio2vo-percentage}, @ref{Customizing
-Coq Multiple File Support}.
+Coq Multiple File Support}. When @code{coq-compile-keep-going} is
+set, vio2vo compilation is scheduled for those files for which
+@code{coqc} compilation was successful.
 
 @emph{Warning}: This mode does only work when you process require
 commands in batches. Slowly single-stepping through require's
@@ -4816,14 +4850,27 @@ The option @code{coq-compile-quick} is described in detail above,
 @ref{Quick compilation and .vio Files}
 
 
+@c TEXI DOCSTRING MAGIC: coq-compile-keep-going
+@defvar coq-compile-keep-going 
+Continue compilation after the first error as far as possible.@*
+Similar to @samp{`make -k}', with this option enabled, the background
+compilation continues after the first error as far as possible.
+With this option disabled, background compilation is
+immediately stopped after the first error.
+
+This option can be set/reset via menu
+@samp{Coq -> Auto Compilation -> Keep going}.
+@end defvar
+
+
 @c TEXI DOCSTRING MAGIC: coq-max-background-compilation-jobs
 @defvar coq-max-background-compilation-jobs 
 Maximal number of parallel jobs, if parallel compilation is enabled.@*
 Use the number of available CPU cores if this is set to
 @code{'all-cpus}. This variable is the user setting. The value that is
-really used is @samp{@code{coq-internal-max-jobs}}. Use @samp{@code{coq-max-jobs-setter}}
+really used is @samp{@code{coq--internal-max-jobs}}. Use @samp{@code{coq-max-jobs-setter}}
 or the customization system to change this variable. Otherwise
-your change will have no effect, because @samp{@code{coq-internal-max-jobs}}
+your change will have no effect, because @samp{@code{coq--internal-max-jobs}}
 is not adapted.
 @end defvar
 
diff --git a/generic/proof-config.el b/generic/proof-config.el
index b4898a35..8ce53168 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1683,7 +1683,12 @@ tries to interrupt the proof process. It is therefore run earlier
 than `proof-shell-handle-error-or-interrupt-hook', which runs
 when the interrupt is acknowledged inside `proof-shell-exec-loop'.
 
-This hook also runs when the proof assistent is killed."
+This hook also runs when the proof assistent is killed.
+
+Hook functions should set the dynamic variable `prover-was-busy'
+to t if there might have been a reason to interrupt. Otherwise
+the generic interrupt handler might issue a prover-not-busy
+error."
   :type '(repeat function)
   :group 'proof-shell)
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 4cb46b0c..51038fa6 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -88,9 +88,11 @@ See the functions `proof-start-queue' and `proof-shell-exec-loop'.")
 
 (defsubst proof-shell-invoke-callback (listitem)
   "From `proof-action-list' LISTITEM, invoke the callback on the span."
-  (condition-case nil
+  (condition-case err
       (funcall (nth 2 listitem) (car listitem))
-    (error nil)))
+    (error
+     (message "error escaping proof-shell-invoke-callback: %s" err)
+     nil)))
 
 (defvar proof-second-action-list-active nil
   "Signals that some items are waiting outside of `proof-action-list'.
@@ -462,7 +464,9 @@ shell buffer, called by `proof-shell-bail-out' if process exits."
 	 (proc     (get-buffer-process (current-buffer)))
 	 (bufname  (buffer-name)))
     (message "%s, cleaning up and exiting..." bufname)
-    (run-hooks 'proof-shell-signal-interrupt-hook)
+    (let (prover-was-busy)
+      ;; hook functions might set prover-was-busy
+      (run-hooks 'proof-shell-signal-interrupt-hook))
     
     (redisplay t)
     (when (and alive proc)
@@ -824,14 +828,18 @@ In the first case, PG will terminate the queue of commands at the first
 available point.  In the second case, you may need to press enter inside
 the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*)."
   (interactive)
-  (unless (proof-shell-live-buffer)
+  (let ((prover-was-busy nil))
+    (unless (proof-shell-live-buffer)
       (error "Proof process not started!"))
-  (unless proof-shell-busy
-    (error "Proof process not active!"))
-  (setq proof-shell-interrupt-pending t)
-  (with-current-buffer proof-shell-buffer
-    (interrupt-process))
-  (run-hooks 'proof-shell-signal-interrupt-hook))
+    ;; hook functions might set prover-was-busy
+    (run-hooks 'proof-shell-signal-interrupt-hook)
+    (if proof-shell-busy
+	(progn
+	  (setq proof-shell-interrupt-pending t)
+	  (with-current-buffer proof-shell-buffer
+	    (interrupt-process)))
+      (unless prover-was-busy
+	(error "Proof process not active!")))))
 
 
 
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index 03af645e..77d3cc33 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -556,7 +556,8 @@ Runs on process status changes and cleans up when prooftree dies."
   "Start the external prooftree process.
 Does also initialize the communication channel and some internal
 variables."
-  (let ((old-proof-tree (get-process proof-tree-process-name)))
+  (let ((process-connection-type nil)	; use pipes, see emacs bug #24531
+	(old-proof-tree (get-process proof-tree-process-name)))
     ;; reset output marker
     (when proof-tree-output-marker
       (set-marker proof-tree-output-marker nil)