aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2017-09-15Merge PR #962: Move dev/doc/changes to Markdown.Maxime Dénès
2017-09-08Move README.ci and link to it from CONTRIBUTING.Théo Zimmermann
2017-09-07Merge PR #968: Better error messages on the CIMaxime Dénès
2017-09-07Merge PR #914: Making the detyper lazyMaxime Dénès
2017-09-05Make AppVeyor generate Windows package.Maxime Dénès
2017-09-05Remove -debug option from Windows build script.Maxime Dénès
It is no longer accepted by Coq's ./configure.
2017-09-05Get sources of cygwin packages after building the installer.Maxime Dénès
2017-09-05Adapt Windows build script to new CoqIDE data installation directory.Maxime Dénès
2017-09-05Print more of the Coq build output.Maxime Dénès
2017-09-05Print Coq build output.Maxime Dénès
2017-09-05In regression test mode, run cygwin setup to install dependencies.Maxime Dénès
2017-09-05Fix Software Foundations build.Maxime Dénès
The Software Foundations archive has been replaced by three volumes.
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager.
2017-08-31Merge PR #999: For BZ#5688, mention hanging issue in ocamldebug and workaroundMaxime Dénès
2017-08-29mention issue with OCAMLRUNPARAM and ocamldebugPaul Steckler
2017-08-29Adapt debugging doc to configure/Makefile changes.Théo Zimmermann
2017-08-29Move debugging to Markdown.Théo Zimmermann
With a minimal diff (so I'm not putting quotes ` ` around all the code).
2017-08-29Move dev/doc/changes to Markdown.Théo Zimmermann
And remove old French part. And move part about the plugin API to the right section.
2017-08-29Merge PR #838: Have coq-dpdgraph ci test print the differencesMaxime Dénès
2017-08-29Merge PR #819: Cleanup old thingsMaxime Dénès
2017-08-24Don't strip the newline, don't use \rJason Gross
Not sure entirely what it was supposed to do, but stripping the newline erased the following line
2017-08-24Swap order of "aggregating..." message and travis_foldJason Gross
Now the folded line starts with "Aggregating..." and not with "---------"
2017-08-24Only display travis_fold: on travisJason Gross
2017-08-18Merge PR #801: Make Travis generate OSX packages.Maxime Dénès
2017-08-17Make Travis generate OSX packages.Maxime Dénès
The packages will be built only for main branches (not pull requests), and are accessible via bintray: https://bintray.com/coq/coq
2017-08-16Mention tclINDEPENDENTL (#349) in dev/doc/changes.Théo Zimmermann
2017-08-15Move the rest of the ci target to a bash fileJason Gross
2017-08-15Better error messages on the CIJason Gross
This makes it so that when a ci target fails, we don't get red herring error messages about .ok files not existing. Since this requires bash, we make a helper script that invokes bash, so as to not depend on bash in general.
2017-08-01Add dev/v8-syntax/check-grammar byproducts to gitignore.Gaëtan Gilbert
2017-08-01Remove obsolete filesGaëtan Gilbert
db_printers just isn't used. api.txt is superseded by the API OCaml interface.
2017-08-01Add .v extension to dev/doc/notes-on-conversionGaëtan Gilbert
This gives syntax highlighting in Coq-aware editors.
2017-08-01Remove dev/TODOGaëtan Gilbert
2017-08-01Fix syntax-v8.tex bad parenthesizingGaëtan Gilbert
Introduced c1e9a27d383688e44ba34ada24fe08151cb5846e
2017-08-01Remove unused Makefiles in dev/tools/Gaëtan Gilbert
They seem unused since 8f4b7f1 (2007).
2017-08-01Have coq-dpdgraph ci test print the differencesJason Gross
This allows better debugging when it fails.
2017-08-01Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Maxime Dénès
2017-07-31Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadMaxime Dénès
2017-07-31Merge PR #746: Timing on ci via coq_makefile for various projectsMaxime Dénès
2017-07-28Merge PR #923: [api] Fix base_include LTAC parts.Maxime Dénès
2017-07-28Merge PR #782: Update API for fiatMaxime Dénès
2017-07-28Merge PR #852: Makefile: fails if some .vo or .cm* file has no sourceMaxime Dénès
2017-07-27[toplevel] Remove long ago deprecated and NOOP options.Emilio Jesus Gallego Arias
Minor clean up, no sense in having these as they do nothing.
2017-07-27[api] Fix base_include LTAC parts.Emilio Jesus Gallego Arias
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-26Merge PR #886: Fixing what was presumably a typo in the naming conventions fileMaxime Dénès
2017-07-25[api] Remove type equalities from API.Emilio Jesus Gallego Arias
This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
2017-07-21Alternate way of doing timing on ciJason Gross
This puts the boilerplate all in one place
2017-07-21Separate make from python script for HoTTJason Gross
HoTT still needs to use the submodule, but this will allow us to more easily see where the build fails, if it does
2017-07-21Display timing data travis for various projectsJason Gross
HoTT, which builds it's own makefile, and supports timing data, makes use of its own timing script. Everything else goes through the coq-bundled timing scripts.
2017-07-20Add AppVeyor infrastructure, launching the test suite under Windows.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:34:55 +0000