coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Replace md5sum/md5 calls by an OCaml program	Jacques-Pascal Deplaix	2017-12-23
\|
*	Merge PR #6217: Do dependencies in 1 command per file class.	Maxime Dénès	2017-12-18
\|\
\| *	Do dependencies in 1 command per file class.	Gaëtan Gilbert	2017-12-15
\| \|
* \|	Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès	2017-12-14
\|\ \
* \ \	Merge PR #6388: Fix issue #6387	Maxime Dénès	2017-12-14
\|\ \ \
* \ \ \	Merge PR #1108: [stm] Reorganize flags	Maxime Dénès	2017-12-13
\|\ \ \ \
* \ \ \ \	Merge PR #6175: Restoring filtering of native files passed to `rm` during ↵	Maxime Dénès	2017-12-13
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	`make clean`.
\| \| \| * \| \|	Fix issue #6387	Martin Vassor	2017-12-11
\| \|_\|/ / / \|/\| \| \| \|
\| * \| \| \|	Restoring filtering of native files passed to `rm` during `make clean`.	Maxime Dénès	2017-12-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was lost during the coq_makefile 1 -> 2 translation.
\| \| * \| \|	[flags] [stm] Reorganize flags.	Emilio Jesus Gallego Arias	2017-12-11
\| \|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We move the main async flags to the STM in preparation for more state encapsulation. There is still more work to do, in particular we should make some of the defaults a parameter instead of a flag.
\| \| * \|	[build] Remove coqmktop in favor of ocamlfind.	Emilio Jesus Gallego Arias	2017-12-10
\| \|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind.
* \| \|	Merge PR #6142: Single quotes break on Windows	Maxime Dénès	2017-12-07
\|\ \ \
* \| \| \|	coq_makefile: pass filenames to coqchk	Ralf Jung	2017-11-29
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate.	Maxime Dénès	2017-11-27
\|\ \ \
\| * \| \|	Fix coq-makefile ocamldoc call when configured with -annotate.	Gaëtan Gilbert	2017-11-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes #6120.
* \| \| \|	Update TimeFileMaker.py to correctly sort timing diffs	Jason Gross	2017-11-22
\|/ / / \| \| \| \| \| \| \| \| \|	Previously, it was reverse-ordering timing diffs.
* \| /	Rename coq-inferior.el -> inferior-coq.el to match provided feature.	Gaëtan Gilbert	2017-11-19
\| \|/ \|/\| \| \| \| \|	Fixes #4988.
\| *	Single quotes break on Windows	Carl Patenaude Poulin	2017-11-11
\|/ \| \| \| \| \| \|	As it is, running a `Makefile.coq` on Windows produces the following error: `cut: ': No such file or directory` Changing to double quotes fixes this.
*	Fix FIXME: use OCaml 4.02 generative functors when available.	Gaëtan Gilbert	2017-11-01
\| \| \| \|	4.02.3 has been the minimal OCaml version for a while now.
*	Merge PR #1144: Fix 5776 - `make` gives `ocamlfind: No such file or ↵	Maxime Dénès	2017-10-12
\|\ \| \| \| \| \| \|	directory` on every execution
\| *	Fix 5776 - `make` gives `ocamlfind: No such file or directory` on every ↵	Maxime Dénès	2017-10-11
\| \| \| \| \| \| \| \|	execution
* \|	Merge PR #1143: fix coq_makefile on cygwin	Maxime Dénès	2017-10-11
\|\ \
\| * \|	Fix BZ#5780: coq_makefile broken under Cygwin	Ralf Jung	2017-10-10
\| \|/
* /	[configure] Support for flambda flags.	Emilio Jesus Gallego Arias	2017-10-10
\|/ \| \| \| \| \| \| \| \|	We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ```
*	TimeFileMaker.py: Allow trailing spaces	Jason Gross	2017-10-06
\| \| \| \| \|	This allows the timing aggregation scripts to handle logs from Travis, which, for some reason, seems to insert trailing spaces.
*	Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵	Maxime Dénès	2017-10-05
\|\ \| \| \| \| \| \|	to escape non-UTF-8 file names)
* \	Merge PR #1059: coq_makefile: make sure compile flags for Coq and ↵	Maxime Dénès	2017-10-05
\|\ \ \| \| \| \| \| \| \| \| \|	coq_makefile are in sync (supersed #1039)…
\| * \|	fix compilation on OCaml < 4.04	Enrico Tassi	2017-10-03
\| \| \|
* \| \|	Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ↵	Maxime Dénès	2017-10-03
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	proof for coqwc
* \ \ \	Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580).	Maxime Dénès	2017-10-03
\|\ \ \ \
\| \| * \| \|	look for Obligation num or Next Obligation to start proof	Paul Steckler	2017-09-26
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #1055: Remove STM vernaculars	Maxime Dénès	2017-09-22
\|\ \ \ \
* \ \ \ \	Merge PR #1070: Remove remaining occurrences of -just-parsing.	Maxime Dénès	2017-09-22
\|\ \ \ \ \
\| \| \| * \| \|	Properly handle "coq_makefile -Q . Foo" (bug #5580).	Guillaume Melquiond	2017-09-21
\| \| \| \| \| \|
\| * \| \| \| \|	Remove remaining occurrences of -just-parsing.	Guillaume Melquiond	2017-09-21
\| \| \|/ / / \| \|/\| \| \|
* / \| \| \|	coq_makefile: dont show errors from failed (ignored) rmdir	Ralf Jung	2017-09-20
\|/ / / /
\| \| * \|	coq_makefile: make sure compile flags for Coq and coq_makefile are in sync	Emilio Jesus Gallego Arias	2017-09-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	E.g. -safe-string is set by configure.ml and made available to both make (via config/Makefile) and coq_makefile (via config/coq_config.ml -> lib/envars.ml -> CoqMakefile.in).
\| * \| \|	Add XML protocol support for Wait.	Maxime Dénès	2017-09-19
\|/ / /
* \| \|	Merge PR #990: Prevent warning about DSTROOT being undefined.	Maxime Dénès	2017-09-15
\|\ \ \ \| \|/ / \|/\| \|
\| \| *	Supporting library names in utf8 in coqdep.	Hugo Herbelin	2017-09-13
\| \|/ \|/\|
* \|	Merge PR #997: coqdoc: Support comments in verbatim output	Maxime Dénès	2017-09-07
\|\ \
* \ \	Merge PR #958: coq_makefile: build/use .cma for packed plugins too	Maxime Dénès	2017-08-31
\|\ \ \
\| * \| \|	coq_makefile: fix .merlin generation (FLG -thread)	Enrico Tassi	2017-08-29
\| \| \| \|
\| * \| \|	coq_makefile: improve documentation	Enrico Tassi	2017-08-29
\| \| \| \|
\| * \| \|	coq_makefile: print error message when coqlib is not set properly	Enrico Tassi	2017-08-29
\| \| \| \|
\| * \| \|	coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxs	Enrico Tassi	2017-08-29
\| \| \| \|
* \| \| \|	Merge PR #773: [flags] Remove XML output flag.	Maxime Dénès	2017-08-29
\|\ \ \ \
\| \| * \| \|	coq_makefile: do not overwrite CAMLFLAGS	Enrico Tassi	2017-08-29
\| \| \| \| \|
\| \| * \| \|	coq_makefile: use dedicated variable for extra packages	Enrico Tassi	2017-08-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	CAMLPKGS is now used to hold extra findlib -packages The previous solution was to use CAMLFLAGS but since 4.05 an invocation of `ocamlopt -pack useless.cmxa foo.cmx -o packedfoo.cmx` fails saying that `useless.cmxa` is not a compilation unit description. CAMLPKGS is used in all `ocamlopt` invocations but for the one performing the packing.
\| \| * \| \|	coq_makefile: build/use .cma for packed plugins	Enrico Tassi	2017-08-29
\| \|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The build chain is always ml -> cmo -> cma ml -> cmx -> cmxa -> cmxs If we are packing, then it becomes ml -> cmo \ ml -> cmo --> cmo -> cma ml -> cmo / ml -> cmxo \ ml -> cmxo --> cmxo -> cmxa -> cmxs ml -> cmxo / The interest of always having a .cma or .cmxa is that such file can carry linking flags, that in findlib terms means which -package was use to build the plugin.