aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
Commit message (Collapse)AuthorAge
* [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
|\
| * adding "user-contrib" directory to ".gitignore"Gravatar Matej Kosik2016-05-19
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\|