| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
Removed documentation for broken -D -w (but the option are still there).
Fixed documentation of others.
|
|
|
|
In OCaml 3.x, the toploop of OCaml was accessible from toplevellib.cma. In
OCaml 4.x, it was replaced by compiler-libs. However, linking with
compiler-libs produces a warning (fatal with OCaml 4.03) as soon as we have a
file named errors.ml or lexer.ml...
The only satisfactory solution seems to be to "pack" compiler libs. But it is
not done currently in the OCaml distribution, and implementing it in coqmktop
at this point would be too risky. So for now, I am disabling the warning until
we hear from the OCaml team. In principle, this clash of modules names can
break OCaml's type safety, so we are living dangerously.
|
|
Like coqc: detect if the current directory was set by options, if not: add
it with empty logical path.
TODO: check if coq_makefile is still correct wrt to this modification, I
think yes, actually it should end being more correct.
|
|
|
|
|
|
(thanks to coq-club, Sep 2015).
|
|
|
|
|
|
|
|
Prior to commit 964d1b70, the dependency files .mllib.d and .mlpack.d
were generated by a call to coqdep using the argument -c (for ocaml
code). While doing some finetuning of the generation of implicit rules,
this commit removed (I think by mistake) this "-c". And without this
-c argument coqdep output nothing on mllib files leading to incorrect
linking of mllibs.
|
|
|
|
|
|
|
|
Characters do not need to be escaped in character ranges. It just had the
effect of matching backslashes four times.
|
|
|
|
"This function is deprecated: the runtime system is now able to print
uncaught exceptions as precisely as Printexc.catch does. Moreover, calling
Printexc.catch makes it harder to track the location of the exception
using the debugger or the stack backtrace facility. So, do not use
Printexc.catch in new code."
|
|
|
|
|
|
Before this commit, coq-tex was reading the .v file and was guessing how
many lines from the coqtop output it should display. Now, it reads the
coqtop output and it guesses how many lines from the .v file it should
display. That way, coq-tex no longer needs to embed a parser; it relies
on coqtop for parsing.
This is much more robust and makes it possible to properly handle script
such as the following one:
Goal { True }
+ { False }.
{ left. exact I. }
As before, if there is a way for a script to produce something that looks
like a prompt (that is, a line that starts with "foo < "), coq-tex will be
badly confused.
|
|
This is only a heuristic and it might cause the tool to become awfully
confused if a line ends with "}" yet this is not the end of a tactic
block. Fixing it would require a full-blown Coq parser inside coq-tex.
Example of crazy output:
Coq < Goal { True }
Coq < 1 subgoal
============================
{True} + {False}
Coq < + { False }.
|
|
The quadratic behaviour of list searching probably appears with small
enough samples. With the advent of usable libraries in Coq, and thus many
possible dependencies, better be safe than sorry.
|
|
|
|
|
|
The search algorithm is not satisfactory though, as it crawls through
all known files to find the proper one. We should rather use some trie-based
data structure, but I'll leave this for a future commit.
|
|
Since commit 2f521670fbd, the Require "file" syntax was not used anymore by
coqtop but the code handling it was still there in coqdep. We finish the work
by erasing the remnant code.
|
|
|
|
|
|
coqc by default uses colors, this allows to disable it. Moreover,
colors are not yet correctly disabled when compiling from emacs (emacs
bugs?), making this option even more useful.
|
|
|
|
For now, warnings are still ignored by default, but this may change. This
commit at least allows to print them whenever desired. The -w syntax is
also opened to future additions to further control the display of
warnings.
|
|
Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.
Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.
If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.
Failure to precompile is a hard error, since it is now explicitly required
by the user.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
bug #4080)
|
|
|
