| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing
changes made to da99355b4d6de31aec5a660f7afe100190a8e683.
Hugo asked for more discussion on this topic, and it was not in the roadmap. I
merged it prematurely because I thought there was a consensus. Also, I missed
that it was changing coq_makefile. Sorry about that.
|
|
|
|
Was PR#229: Bytecode compilation in a new 'make byte' rule apart from 'make world'
|
|
match.""
We apply this patch to trunk so that it is integrated in 8.6.
This reverts commit 0eb08b70f0c576e58912c1fc3ef74f387ad465be.
|
|
|
|
not in pl2.
|
|
|
|
We apply this patch to trunk for integration in 8.6 instead.
This reverts commit 715f547816addf3e2e9dc288327fcbcee8c6d47f.
|
|
|
|
Was PR#228: fix coqide double module linking (error on OCaml 4.03)
Fixes #4747: Problem building Coq 8.5pl1 with OCaml 4.03.0: Fatal warnings
triggered by CoqIDE
|
|
This was implemented in anticipation of a part of PR#164 that we decided not to
merge.
|
|
|
|
Was PR#226: CErrors & CClosure
|
|
lib/cErrors.ml)
|
|
For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
|
|
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
|
|
|
Was PR#231: Separate flags for fix/cofix/match reduction and clean reduction
function names, itself a revision of PR#117: Isolating flags for cofix/fix
reduction + adjusting names of reduction functions to what they do
|
|
|
|
whd_zeta now takes an evar_map and looks in evar instances. This changes
the behavior of whd_zeta e.g. on let x := ?t in x
|
|
|
|
This is a reimplementation of Hugo's PR#117.
We are trying to address the problem that the name of some reduction functions
was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in
reduction). Like PR#117, we are careful that no function changed semantics
without changing the names. Porting existing ML code should be a matter of
renamings a few function calls.
Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX
collectively denominated iota.
We renamed the following functions:
Closure.betadeltaiota -> Closure.all
Closure.betadeltaiotanolet -> Closure.allnolet
Reductionops.beta -> Closure.beta
Reductionops.zeta -> Closure.zeta
Reductionops.betaiota -> Closure.betaiota
Reductionops.betaiotazeta -> Closure.betaiotazeta
Reductionops.delta -> Closure.delta
Reductionops.betalet -> Closure.betazeta
Reductionops.betadelta -> Closure.betadeltazeta
Reductionops.betadeltaiota -> Closure.all
Reductionops.betadeltaiotanolet -> Closure.allnolet
Closure.no_red -> Closure.nored
Reductionops.nored -> Closure.nored
Reductionops.nf_betadeltaiota -> Reductionops.nf_all
Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta
Reductionops.whd_betadeltaiota -> Reductionops.whd_all
Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet
Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack
Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack
Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack
Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state
Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state
Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state
Reductionops.whd_eta -> Reductionops.shrink_eta
Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all
Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all
And removed the following ones:
Reductionops.whd_betaetalet
Reductionops.whd_betaetalet_stack
Reductionops.whd_betaetalet_state
Reductionops.whd_betadeltaeta_stack
Reductionops.whd_betadeltaeta_state
Reductionops.whd_betadeltaeta
Reductionops.whd_betadeltaiotaeta_stack
Reductionops.whd_betadeltaiotaeta_state
Reductionops.whd_betadeltaiotaeta
They were unused and having some reduction functions perform eta is confusing
as whd_all and nf_all don't do it.
|
|
|
|
But there are still bugs with Declare Implicit Tactic, which should
probably rather be reimplemented with ltac:(tac).
Indeed, it does support evars in the type of the term, and
solve_by_implicit_tactic should transfer universe constraints to the
main goal. E.g., the following still fails, at Qed time.
Definition Foo {T}{a : T} : T := a.
Declare Implicit Tactic eassumption.
Goal forall A (x : A), A.
intros.
apply Foo.
Qed.
|
|
This allows to grant a wish by Hugo: to build coqtop.byte and prelude
with it, you could do:
make -j BEST=byte states
|
|
make install does not install these *.cm(o|a) files either.
You could always do manually :
- make bytefiles : to build the bytecode *.cm(o|a) files
- make install-byte : to install these files
- make byte : to compile the whole development with the bytecode version
of Coq (this builds the *.cm(o|a) files, but also the .vo via coqc -byte).
Technically, the behavior of make is controlled by the OPT variable,
which could be -byte or -opt. For instance, 'make byte' corresponds to a
'make OPT:=-byte'
Note that coqdep is used with the new option "-dyndep var" : when seeing
a Declare ML Module "foo", "coqdep -dyndep var" does not decide whether to
depend on foo.cma or foo.cmxs, but rather use some Makefile variables such
as foo$(DYNLIB), whose content is later set according to $(OPT)
|
|
On a machine for which ocamlopt is available, the make world will now
perform bytecode compilation only in grammar/ (up to the syntax
extension grammar.cma), and then exclusively use ocamlopt.
In particular, make world do not build bin/coqtop.byte.
A separate rule 'make byte' does it, as well as bytecode plugins and
things like dev/printers.cma.
'make install' deals only with the part built by 'make', while a new
rule 'make install-byte' installs the part built by 'make byte'.
IMPORTANT: PLEASE AVOID doing things like 'make -j world byte' or any
parallel mix of native and byte rules. These are known to crash sometimes,
see below. Instead, do rather 'make -j && make -j byte'.
Indeed, apart from marginal compilation speed-up for users not interested
in byte versions, the main reason for this commit is to discourage any
simultaneous use of OCaml native and byte compilers. Indeed, ocamlopt and
ocamlc will both happily destroy and recreate .cmi for .ml files with no .mli,
and in case of parallel build this may happen at the very moment another
ocaml(c|opt) is accessing this .cmi. Until now, this issue has been
handled via nasty hacks (see the former MLWITHOUTMLI and HACKMLI vars in
Makefile.build). But these hacks weren't obvious to extend to ocamlopt
-pack vs. ocamlopt -pack.
coqdep_boot takes a "-dyndep" option to control precisely how a Declare ML
Module influences the .v.d dependency file. Possible values are:
-dyndep opt : regular situation now, depends only on .cmxs
-dyndep byte : no ocamlopt, or compilation forced to bytecode, depends on .cm(o|a)
-dyndep both : earlier behavior, dependency over both .cm(o|a) and .cmxs
-dyndep none : interesting for coqtop with statically linked plugins
-dyndep var : place Makefile variables $(DYNLIB) and $(DYNOBJ) in .v.d
instead of extensions .cm*, so that the choice is made in the rest of the
makefile (see next commit about coq_makedile)
NB: two extra mli added to avoid building unecessary .cmo during 'make world',
without having to use the ocamldep -native option.
NB: we should state somewhere that coqmktop -top won't work unless
'make byte' was done first
|
|
See 4865.v for details.
|
|
|
|
|
|
|
|
|
|
Unset Program Generalized Coercion to avoid coercion of general
applications.
Unset Program Cases to deactivate generation equalities and
disequalities of cases.
|
|
|
|
|
|
|
|
|
|
|
|
When using Record and an explicit sort constraint, the
universe was wrongly made flexible and minimized.
|
|
For better error messages. The API change is
backwards compatible, using a new optional argument.
|
|
When declaring the universes of a lemma explicitely, throw an error if
after minimization the type of a lemma still refers to unbound
universes. This is a fix and an incompatibility, but scripts
will be backwards compatible themselves.
Fix another minor bug in treating universe binders for (Co)Fixpoint.
|
|
Was PR#213: New warnings machinery
|
|
|
|
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
|
This allows a work-around for bug #4819,
https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
|
|
Linking the same module twice in OCaml can have problematic unintended
consequences and lead to hard-to-understand bugs, see
http://caml.inria.fr/mantis/view.php?id=4231
http://caml.inria.fr/mantis/view.php?id=5461
OCaml has long warned when double-linking happens
Warning 31: files FOO and BAR both define a module named Baz
In 4.03 this error was turned into a warning by default.
Coqide does double-linking by passing both
xml_{lexer,parser,printer}.cmo and lib/clib.cma that already contains
these compilation units to bin/coqide.byte. To fix compilation of
Coqide under 4.03, the present patch removes the .cmo from the
command-line arguments.
P.S.: I checked that this patch applies cleanly to the current trunk
(b161ad97fdc01ac8816341a089365657cebc6d2b). It should also be possible
to add it as a patch on top of the 8.5 archives (for example those
distributed through OPAM) to make them compile under 4.03.
|
|
This reverts commit 925d258d7d03674c601a1f3832122b3b4b1bc9b0.
I forgot that Jenkins gave me a spurious success when trying to build this PR.
There are a few rough edges to fix, so reverting meanwhile. The Jenkins issue
has been fixed by Matej. Sorry for the noise.
|
|
Otherwise we may backtrack on the resolution in a
by which seems strange.
|
|
Was PR#213: New warnings machinery
|
