aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge branch 'divided-makefile' into trunkGravatar Pierre Letouzey2016-06-08
|\
| * Makefile.build split in many smaller files : Makefile.{ide,checker,dev,install}Gravatar Pierre Letouzey2016-06-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | General idea : Makefile.build was far too big to be easy to grasp or maintain, with information scattered everywhere. Let's try to tidy that! Normally, this commit is transparent for the user. We simply regroup some parts of Makefile.build in several new dedicated files: - Makefile.ide - Makefile.checker - Makefile.dev (for printers, revision, extra partial targets, otags) - Makefile.install These new files are "included" at the start of Makefile.build, to provide the same behavior as before, but with a Makefile.build shrinked by 50% (to approx 600 lines). Makefile.build now handles in priority the build of coqtop, minor tools, theories and plugins. Note: this is *not* a separate build system for coqchk nor coqide, even if this can be seen as a first step in this direction (won't be easy anyway to continue, due to the sharing of various stuff in lib and more). In particular Makefile.{coqchk,ide} may rely here and there on some generic rules left in Mafefile.build. Conversely, be sure to prefix rules in Makefile.{coqchk,ide} by checker/... or ide/... in order to avoid interferences with generic rules. Makefile.common is still there, but quite simplified. For instance, some variables that were used only once (e.g. lists of cmo files to link in the various tools) are now defined in Makefile.build, directly where they're needed. THEORIESVO and PLUGINSVO are made directly out of the theories/*/vo.itarget and plugins/*/vo.itarget files, no long manual list of subdirs anymore. Specific sub-targets such as 'reals' still exist, but in Makefile.dev, and they aren't mandatory. Makefile.doc is augmented by the rules building the documentation of the sources via ocamldoc. This classification attempt could probably be improved. For instance, the install rules for coqide are currently in Makefile.ide, but could also go in Makefile.install. Note that I've removed install-library-light which was broken anyway (arith isn't self-contained anymore).
| * Makefile: avoid overwriting test.ml when testing grammar.cmaGravatar Pierre Letouzey2016-06-08
| |
| * Makefile: make clean now removes the .coq-native subdirsGravatar Pierre Letouzey2016-06-08
|/ | | | | | More precisely, we first remove *.native, *.cm*, *.o, which should normally consistute the only content of these .coq-native directories, and then remove these directories if they're indeed empty
* Officially discontinue the experimental coq build via ocamlbuildGravatar Pierre Letouzey2016-06-08
| | | | | | | | | It has been accidentaly broken since early 2014 (and especially in 8.5), no easy repair, I won't devote any more hours to this stuff. Moreover no one seems to care apart from Emilio, but he's ok to work on this in a separate repository or branch. I left a dev/doc/ocamlbuild.txt file with a few words about this experiment.
* proofs/proofs.mllib: no more proof_errors !Gravatar Pierre Letouzey2016-06-08
|
* Search interface revisions.Gravatar Pierre-Marie Pédrot2016-06-07
|\
| * Removing the convenience functions from the Search API.Gravatar Pierre-Marie Pédrot2016-06-07
| |
* | Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr/gitroot/coq/coq into trunkGravatar Matej Kosik2016-06-07
|\ \
| * \ coq_makefile : minor reworkGravatar Pierre Letouzey2016-06-07
| |\ \
| | * | Coq_makefile: code cleanup (less long lines, etc)Gravatar Pierre Letouzey2016-06-07
| | | |
| | * | coq_makefile: List.iteri is now standard since OCaml 4.00Gravatar Pierre Letouzey2016-06-07
| | | |
| | * | coq_makefile : short display of commands executed by makeGravatar Pierre Letouzey2016-06-07
| | | | | | | | | | | | | | | | | | | | | | | | This purely cosmetic effect is obtained by the same variables $(SHOW) and $(HIDE) as in the main Makefile of Coq. If you prefer the earlier raw output : make VERBOSE=1
| | * | coq_makefile: add some -ml-synonym to the ocamldep rulesGravatar Pierre Letouzey2016-06-07
| |/ / | | | | | | | | | | | | Without this, dependencies upon a .ml4 (or a .mlpack) won't be handled correctly.
* | | typoGravatar Matej Kosik2016-06-07
| | |
* | | typographyGravatar Matej Kosik2016-06-07
| | |
| * | printing.mllib: remove some other .mli-only from a .mllibGravatar Pierre Letouzey2016-06-07
| | |
| * | Test for #4787.Gravatar Hugo Herbelin2016-06-07
| | |
| * | Fixing #4787 (Unset Bracketing Last Introduction Pattern not working).Gravatar Hugo Herbelin2016-06-07
|/ /
* | Relying instead on the Coq85 inclusion!Gravatar Hugo Herbelin2016-06-06
| |
* | Mode "Bracketing Last Introduction Pattern" is on for 8.4Gravatar Hugo Herbelin2016-06-06
| | | | | | | | and global for 8.4 and 8.5.
* | Mode "Regular Subst Tactic" is on in 8.6.Gravatar Hugo Herbelin2016-06-06
| |
* | Merge remote-tracking branch 'github/pr/118' into trunkGravatar Maxime Dénès2016-06-06
|\ \
* | | About printing of traces of failures while calling ltac code.Gravatar Hugo Herbelin2016-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | An Ltac trace printing mechanism was introduced in 8.4 which was inadvertedly modified by a series of commits such as 8e10368c3, 91f44f1da7a, ... It was also sometimes buggy, iirc, when entering ML tactics which themselves were calling ltac code. It got really bad in 8.5 as in: Tactic Notation "f" constr(x) := apply x. Ltac g x := f x. Goal False. idtac; f I. (* bad location reporting *) g I. (* was referring to tactic name "Top.Top#<>#1" *) which this commit fixes. I don't have a clear idea of what would be the best ltac tracing mechanism, but to avoid it to be broken without being noticed, I started to add some tests. Eventually, it might be worth that an Ltac expert brainstrom on it!
* | | xmlprotocol: fix unmarshaling of Feedback.MessageGravatar Enrico Tassi2016-06-06
| | |
* | | xmlprotocol: uncomment marshalling code for custom messageGravatar Enrico Tassi2016-06-06
| | |
* | | xmlprotocol: Marshal_error carries the reasonGravatar Enrico Tassi2016-06-06
| | |
* | | Adding the Print Ltac Signatures command.Gravatar Pierre-Marie Pédrot2016-06-05
|\ \ \
| * | | Adding the Print Ltac Signature command.Gravatar Pierre-Marie Pédrot2016-06-05
|/ / /
* | | Remove Q_constr from grammar folder.Gravatar Pierre-Marie Pédrot2016-06-05
|\ \ \
| * | | Removing the Q_constr file.Gravatar Pierre-Marie Pédrot2016-06-05
| | | |
| * | | Moving Hipattern to a regular ML file.Gravatar Pierre-Marie Pédrot2016-06-05
| | | |
| * | | Removing PATTERN uses in Hipattern.Gravatar Pierre-Marie Pédrot2016-06-05
|/ / /
* | | Merge remote-tracking branch 'github/pr/184' into trunkGravatar Maxime Dénès2016-06-04
|\ \ \
* \ \ \ Remove a few tactics from the Tacexpr AST.Gravatar Pierre-Marie Pédrot2016-06-03
|\ \ \ \ | | | | | | | | | | | | | | | | | | | | Note that this breaks a few badly written scripts using intro in strict mode without providing an existing identifier.
| * | | | Removing "rename" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
| | | | |
| * | | | Removing "exact" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
| | | | |
| * | | | Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note that this breaks the compatibility, in a beneficial way I believe. Tactics defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction on a local identifier anymore. They must use the "fresh" primitive instead.
| * | | | Removing "double induction" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
|/ / / /
* | | | Merge remote-tracking branch 'github/pr/159' into trunkGravatar Maxime Dénès2016-06-03
|\ \ \ \
* | | | | Fix build of documentation (broken for four months).Gravatar Guillaume Melquiond2016-06-03
| | | | |
* | | | | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2016-06-03
|\ \ \ \ \
| * | | | | Fix proof terminators not being detected in presence of curly brackets (bug ↵Gravatar Guillaume Melquiond2016-06-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | #4770). This also fixes comments not being properly skipped when looking for eol.
| * | | | | Make "coqdoc -g --parse-comments" behave properly (bug #4773).Gravatar Guillaume Melquiond2016-06-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As a side effect, there should be a small speedup when ignoring comments. This commit also fixes two bugs related to handling "$$" and "#" in comments.
* | | | | | Please never mention .mli-only file in *.mllib (or future *.mlpack)Gravatar Pierre Letouzey2016-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This breaks compilation via ocamlbuild, and also leads to awkward commands via make
| | | * | | Add documentation to the low-level `Pp` functions.Gravatar Emilio Jesus Gallego Arias2016-06-02
| |_|/ / / |/| | | | | | | | | | | | | | Thanks to HH for pointing it out.
* | | | | Move XML serialization to ide/ folder.Gravatar Pierre-Marie Pédrot2016-06-02
|\ \ \ \ \
| * | | | | Move ide serialization libraries from lib/ to ide/Gravatar Emilio Jesus Gallego Arias2016-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This makes the core free from particular protocol choices. It should help with the ppx serialization project and shrinks clib.cma a bit.
| * | | | | Encapsulate xml serialization in xmlprotocol.mliGravatar Emilio Jesus Gallego Arias2016-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This eases the task of replacing/improving the serializer, as well as making it more resistant. See pitfalls below: Main changes are: - fold `message` type into `feedback` type - make messages of type `Richpp.richpp` so we are explicit about the content being a rich document. - moved serialization functions for messages and stateid to `Xmlprotocol` - improved a couple of internal API points (`is_message`). Tested.
| * | | | | Move serialization functions out of StmGravatar Emilio Jesus Gallego Arias2016-06-02
|/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Serialization should be specific to each particular backend, so we let the Stm clients choose how the send the nodes. This should be quite safe to pull in. Test suite passes. Related to #180
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 22:48:57 +0000