| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
enough
In particular, its interface might still change (in interaction with interested
colleagues). So let's not give it too much visibility yet. Instead, I'll turn
it as an opam packages for now.
|
|
|
|
|
|
|
|
|
|
|
|
Also remove AsyncProofs.tex from the list of preprocessed files, as it is
doubtful it will ever contains Coq scripts.
|
|
|
|
Broke the build.
This reverts commit ef6459b00999a29183edc09de9035795ff7912e9.
|
|
|
|
|
|
NB: this is work-in-progress, there is currently only one
provided implementation (MMapWeakList).
In the same spirit as MSets w.r.t FSets, the main difference between
MMaps and former FMaps is the use of a new version of OrderedType
(see Orders.v instead of obsolete OrderedType.v).
We also try to benefit more from recent notions such as Proper.
For most function specifications, the style has changed : we now use
equations over "find" instead of "MapsTo" predicates, whenever possible
(cf. Maps in Compcert for a source of inspiration). Former specs are
now derived in FMapFacts, so this is mostly a matter of taste.
Two changes inspired by the current Maps of OCaml:
- "elements" is now "bindings"
- "map2" is now "merge" (and its function argument also receives a key).
We now use a maximal implicit argument for "empty".
|
|
NB: this is work-in-progress, there is currently only one
provided implementation (MMapWeakList).
In the same spirit as MSets w.r.t FSets, the main difference between
MMaps and former FMaps is the use of a new version of OrderedType
(see Orders.v instead of obsolete OrderedType.v).
We also try to benefit more from recent notions such as Proper.
For most function specifications, the style has changed : we now use
equations over "find" instead of "MapsTo" predicates, whenever possible
(cf. Maps in Compcert for a source of inspiration). Former specs are
now derived in FMapFacts, so this is mostly a matter of taste.
Two changes inspired by the current Maps of OCaml:
- "elements" is now "bindings"
- "map2" is now "merge" (and its function argument also receives a key).
We now use a maximal implicit argument for "empty".
|
|
together with the tactic monad.
The move is not complete yet, because some file candidates for this directory
have almost useless dependencies in other ones that should not be moved.
|
|
In particular:
- abstracting the code using calls to Unix opendir, stat, and closedir,
- uniformly using warnings when a directory does not exist (coqtop was
ignoring silently and coqdep was exiting via handle_unix_error),
- uniformly expecting paths in Unix format and warning otherwise.
|
|
|
|
|
|
(Sorry, was not intended to be pushed)
This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
|
|
In particular:
- abstracting the code using calls to Unix opendir, stat, and closedir,
- uniformly using warnings when a directory does not exist (coqtop was
ignoring silently and coqdep was exiting via handle_unix_error).
|
|
|
|
|
|
PIDE based user interfaces use glob files and source files to
implement hyperlinks
|
|
- proofworkertop to deal with proof tasks
- tacworkertop to deal with par: tactics
- queryworkertop to deal with queries (next commit)
|
|
|
|
|
|
Left a README, just in case someone will discover the remnants of it
decades from now.
|
|
CoqIDE seems to work, but for random pauses that make you think
of a thread deadlock, but then, after a few seconds, things make
progress again. This happens only seldom on my virtual machine.
|
|
|
|
|
|
par: distributes the goals among a number of workers given
by -async-proofs-tac-j (defaults to 2).
|
|
|
|
|
|
The created bundle contains only coqide and gtk (no coqtop, no stdlib)
|
|
lib/interface split into:
- lib/feedback
subscribe-based feedback bus (also used by coqidetop)
- ide/interface
definition of coqide protocol messages
lib/pp
structured info/err/warn messages
lib/serialize split into:
- lib/serialize
generic xml serialization (list, pairs, int, loc, ...)
used by coqide but potentially useful to other interfaces
- ide/xmlprotocol
serialization of protocol messages as in ide/interface
the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/
|
|
User interface writers can drop a footop.cmxs in $(COQLIB)/toploop/
and pass -toploop footop to customize the coq main loop.
A toploop must set Coqtop.toploop_init and Coqtop.toploop_run to
functions respectively initializing the toploop (and parsing toploop
specific arguments) and running the main loop itself.
For backward compatibility -ideslave and -async-proofs worker do
set the toploop to coqidetop and stmworkertop respectively.
|
|
Should decrease the noise level in the bench.
|
|
files around. A bunch of files from lib/ that were only used in the STM were
moved, as well as part of toplevel/ related to the STM.
|
|
This reverts commit f694544d016b085b3cd10007b9f7716ae2c3b022.
This commit was wrong, since (at least) the highparsing part depends
on the toplevel directory. I still didn't had time to fix that, so
in the meantime let's revert it.
|
|
|
|
In last commit, we used grep to decide whether a .ml4 could be
compiled during the initial phase of not. Instead, we now rely on
a simpler directory dichotomy:
- config lib kernel library pretyping interp parsing grammar
are considered initial (and shouldn't contain grammar-dependent .ml4),
see $(GRAMSRCDIRS) in Makefile.common
- the grammar-dependent .ml4 could be in any other directories
Currently, they are in: tactics toplevel plugins/*
|
|
|
|
The Spawn and Spawned modules factor the operation of spawning
a process. Both synchronous and asynchronous channels are supported.
Both threaded and glib like main loop models are supported. Still,
not all combinations are truly tested not equipped with a decent API:
only async + glib and sync + thread are, since these are the models we
use for coqide<->coqtop and coqtop<->worker respectively.
|
|
|
|
* vars.mli was mentionning Term instead of Constr, leading to a dep cycle
* Having a file named toplevel/toplevel.ml isn't a good idea when we also
have a toplevel/toplevel.mllib that ought to produce a toplevel.cma.
We rename toplevel.ml into Coqloop.ml
* Extra cleanup of toplevel.mllib :
- Ppextra isn't anywhere around (?!)
- Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway
- Vernacexpr is a .mli and shouldn't appear in an .mllib
* During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml)
* A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread
for coqchk).
|
|
I put it in a new chapter of the Addendum of the manual. Which is meant to be dedicated to plugins with short documentation.
|
|
A small plugin to support program deriving (à la Richard Bird) in Coq.
It's fairly simple:
Require Coq.Derive.Derive.
Derive f From g Upto eq As h.
Produces a goal (actually two, but the first one is automatically shelved):
|- eq g ?42
And closing the proof produces two definitions: f is instantiated with the value of ?42 (it's always transparent). And h is instantiated with the content of the proof (it is transparent or opaque depending on whether the proof was closed with Defined or Qed).
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 85f007b7-540e-0410-9357-904b9bb8a0f7
|
