aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
Commit message (Collapse)AuthorAge
* [ide] Move common protocol library to its own folder/object.Gravatar Emilio Jesus Gallego Arias2018-05-24
| | | | | | | | | | | | | | | | | The `ide` folder contains two different binaries, the language server `coqidetop` and `coqide` itself. Even if these binaries are in the same folder, the only thing they have in common is that they link to the protocol files. In the OCaml world, having "doubly" linked files in the same project is considered a bit of an ugly practice, and some build tools such as Dune disallow it.q Thus, to clean up the build, we move the common protocol files to its own library `ideprotocol`. This helps towards Dune integration and towards having an IDE standalone target, such as the one that was implemented here: https://github.com/ejgallego/coqide-exp
* add unit tests to test suiteGravatar Paul Steckler2018-05-16
|
* [doc] Update Sphinx build instructions for Debian derivatives.Gravatar Emilio Jesus Gallego Arias2018-04-30
| | | | | | We update the instructions a bit providing the name of the Debian packages, we also mention Nix and add to .gitignore a Sphinx-autogenerated file.
* Remove LaTeX refman, now that migration to Sphinx is completeGravatar Maxime Dénès2018-04-16
|
* [Sphinx] Read version number from configureGravatar Maxime Dénès2018-03-13
|
* Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | longer use camlp4.
* Ignore generated test-suite/output/MExtraction.outGravatar Jason Gross2017-12-31
|
* [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
| | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
* [make] remove unneeded generated file "tolink.ml"Gravatar Emilio Jesus Gallego Arias2017-12-10
| | | | | | | | | | When statically linking plugins, the "DECLARE PLUGIN" macro takes care of properly setting up the loaded module table. This setup was also done by `coqmktop`, thus in order to ease bisecting, we didn't take care of it in the `coqmktop` deprecation. Fixes #6364.
* Extend .gitignore for coqdoc test-suite.Gravatar Théo Zimmermann2017-08-21
|
* Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵Gravatar Maxime Dénès2017-08-16
|\ | | | | | | wrongly tagged as keywords
| * Adding a coqdoc target to test-suite.Gravatar Hugo Herbelin2017-07-17
| | | | | | | | | | | | | | One file was already ready for testing. We add another one. Note that we have to remove the machine-dependent lines in the output tex files.
* | Add timing scriptsGravatar Jason Gross2017-07-11
|/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit adds timing scripts from https://github.com/JasonGross/coq-scripts/tree/master/timing into the tools folder, and integrates them into coq_makefile and Coq's makefile. The main added makefile targets are: - the `TIMING` variable - when non-empty, this creates for each built `.v` file a `.v.timing` variable (or `.v.before-timing` or `.v.after-timing` for `TIMING=before` and `TIMING=after`, respectively) - `pretty-timed TGTS=...` - runs `make $(TGTS)` and prints a table of sorted timings at the end, saving it to `time-of-build-pretty.log` - `make-pretty-timed-before TGTS=...`, `make-pretty-timed-after TGTS=...` - runs `make $(TGTS)`, and saves the timing data to the file `time-of-build-before.log` or `time-of-build-after.log`, respectively - `print-pretty-timed-diff` - prints a table with the difference between the logs recorded by `make-pretty-timed-before` and `make-pretty-timed-after`, saving the table to `time-of-build-both.log` - `print-pretty-single-time-diff BEFORE=... AFTER=...` - this prints a table with the differences between two `.v.timing` files, and saves the output to `time-of-build-pretty.log` - `*.v.timing.diff` - this saves the result of `print-pretty-single-time-diff` for each target to the `.v.timing.diff` file - `all.timing.diff` (`world.timing.diff` and `coq.timing.diff` in Coq's own Makefile) - makes all `*.v.timing.diff` targets N.B. We need to make `make pretty-timed` fail if `make` fails. To do this, we need to get around the fact that pipes swallow exit codes. There are a few solutions in https://stackoverflow.com/questions/23079651/equivalent-of-pipefail-in-gnu-make; we choose the temporary file rather than requiring the shell of the makefile to be bash.
* Update .gitignore with doc/tutorial/Tutorial.v.outGravatar Jason Gross2017-06-30
|
* Ignore all PDF files.Gravatar Théo Zimmermann2017-06-22
| | | | | | Rules for ignoring *some* PDF files had been added one by one to `.gitignore` but some were still missing (for the corresponding latex files in `dev`). This rule is actually better since we are not tracking any PDF file.
* Makefile.build : cleanup now that micromega.ml isn't generated + sync check ↵Gravatar Pierre Letouzey2017-06-14
| | | | | | | of this file There is now a warning if the content of micromega.ml isn't what MExtraction.v would produce.
* BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
| | | | | | See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude.
* Merge PR#743: Update .gitignoreGravatar Maxime Dénès2017-06-13
|\
* | Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to ↵Gravatar Matej Košík2017-06-12
| | | | | | | | generate them later.
* | Add support for "-bypass-API" argument of "coq_makefile"Gravatar Matej Košík2017-06-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
| * Update .gitignoreGravatar Jason Gross2017-06-07
| |
* | Put "ssreflect" behind "API".Gravatar Matej Košík2017-06-07
| |
* | Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
|/
* extract "plugins/micromega/micromega.ml{,i}" files from ↵Gravatar Matej Kosik2017-06-01
| | | | "plugins/micromega/MExtraction.v"
* Add some test-suite generated files to .gitignoreGravatar Jason Gross2017-05-30
|
* test suite for coq_makefile2Gravatar Enrico Tassi2017-05-23
|
* ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mliGravatar Enrico Tassi2017-05-23
| | | | The .mli only acknowledges the current API. I'm not guilty your honor!
* test suite for coq_makefileGravatar Enrico Tassi2017-05-23
|
* [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| | | | | | | | We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
* Improve build of travis target on local machine.Gravatar Théo Zimmermann2017-03-10
| | | | | - Move the git clones to a specific subfolder to avoid pollution. - Do not fail when git clone already exist (but make sure it is up-to-date).
* Fix .gitignore.Gravatar Pierre-Marie Pédrot2017-02-17
|
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\
| * Update .gitignore with new names for psatz cachesGravatar Jason Gross2016-10-24
| |
* | enriching ".gitignore"Gravatar Matej Kosik2016-10-19
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\|
| * Updating .gitignore.Gravatar Hugo Herbelin2016-09-09
| |
* | No more dev/printers.cmaGravatar Pierre Letouzey2016-07-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This file was only used during ocamldebug sessions (in the dev/db script). It was containing a large subset of the core cma files, up to the printing functions. There were a few notable exceptions, for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug. But printers.cma was troublesome to maintain : almost each time an ML file was added/removed/renamed in the core of Coq, dev/printers.mllib had to be edited, in addition to the directory-specific .mllib (kernel/kernel.mllib and co). So I propose here to kill this file, and put instead in dev/db several "load_printer" of the core cma files. For that to work, we need to compile kernel/kernel.cma with the right -dllib and -dllpath options, but that shouldn't hurt (on the contrary). We also source now the camlpX cma in dev/db, via a new generated file dev/camlp4.dbg containing a load_printer of either gramlib.cma or camp4lib.cma. If one doesn't want to perform the whole "source db" at the start of an ocamldebug session, then the former "load_printer printers.cma" could be replaced by: source core.dbg load_printer top_printers.cmo See for instance the minimal dev/base_db.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-07-13
|\|
| * .gitignore: no more generated grammar/*.ml filesGravatar Pierre Letouzey2016-07-12
| |
| * ".gitignore" updateGravatar Matej Kosik2016-07-12
| |
* | dummy commit --- I just need a hash that does not belong to v8.6 branchGravatar Matej Kosik2016-07-07
|/
* Ignore generated .ml file for ssrmatchingGravatar Enrico Tassi2016-06-16
|
* configure: use ln on linux and cp on windowsGravatar Enrico Tassi2016-06-14
|
* Merge branch "LtacProf for trunk" (PR #165).Gravatar Pierre-Marie Pédrot2016-06-14
|\
* | Compilation via pack for plugins of the stdlibGravatar Pierre Letouzey2016-06-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For now, the pack name reuse the previous .cma name of the plugin, (extraction_plugin, etc). The earlier .mllib files in plugins are now named .mlpack. They are also handled by bin/ocamllibdep, just as .mllib. We've slightly modified ocamllibdep to help setting the -for-pack options: in *.mlpack.d files, there are some extra variables such as foo/bar_FORPACK := -for-pack Baz when foo/bar.ml is mentioned in baz.mlpack. When a plugin is calling a function from another plugin, the name need to be qualified (Foo_plugin.Bar.baz instead of Bar.baz). Btw, we discard the generated files plugins/*/*_mod.ml, they are obsolete now, replaced by DECLARE PLUGIN. Nota: there's a potential problem in the micromega directory, some .ml files are linked both in micromega_plugin and in csdpcert. And we now compile these files with a -for-pack, even if they are not packed in the case of csdpcert. In practice, csdpcert seems to work well, but we should verify with OCaml experts.
| * LtacProf for Coq trunkGravatar Jason Gross2016-06-05
|/ | | | | | This add LtacProfiling. Much of the code was written by Tobias Tebbi (@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq v8.5 and Coq trunk.
* 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
|
* 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.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-20
|\