aboutsummaryrefslogtreecommitdiff
path: root/etc/utils
AgeCommit message (Collapse)Author
2021-03-25fix gotpodCyril Cohen
2021-03-15fixup gitpod configCyril Cohen
2020-06-27Fix bugs in hierarchy.mlKazuhiko Sakaguchi
- pass `Unix.environment ()` to `coqtop` to preserve the parent process environment, - check the exit status of `coqtop` and report an error if it is wrong, - do not rely on `ssrfun.id` in the `check_join` tactic, and - improve the error message for missing unification hints.
2020-06-10Generated opam packages allow coq-dev againCyril Cohen
As a result of [a discussion on Zulip](https://coq.zulipchat.com/#narrow/stream/237665-math-comp-devs/topic/MathComp.201.2E11.2E0.20OPAM.20packages.20Coq.20compatibility) Reverts "removing opam `| (= "dev")` for released packages" (commit 313e44316177c918b363c118f15297e08d13eb4e).
2020-06-09removing opam `| (= "dev")` for released packagesCyril Cohen
2020-05-27URL in httpsCyril Cohen
2020-04-15fix packagerCyril Cohen
2020-03-15Fix hierarchy.ml to compute the transitive closure of a hierarchyKazuhiko Sakaguchi
2019-12-02take advantage of opam variables and their default valuesYves Bertot
2019-10-02Fix and improve the test suite and MakefileKazuhiko Sakaguchi
- improve an error message produced by the `check_join` tactic, - fix the build of the test suite: `make test-suite`, and - add a new rule `only` to build a subset of MathComp.
2019-04-30Reimplement the hierarchy related tools in OCamlKazuhiko Sakaguchi
The functionalities of the structure hierarchy related tools `hierarchy-diagram` and `hierarchy_test.py` are provided by an OCaml script `hierarchy.ml`. `test_suite/hierarchy_test.v` is deleted. Now make can generate it.
2019-04-08switching to opam 2.0 formatCyril Cohen
2019-04-08New test cases generation: corrent implementation of least common childrenKazuhiko Sakaguchi
Add a new option `-raw-inheritances` to `hierarchy-diagram` to generate an intermediate file for `hierarchy_test.py`. So the typical usage is: $ python3.5 etc/utils/hierarchy_test.py \ <(etc/utils/hierarchy-diagram -raw-inheritances -R mathcomp mathcomp) \ > mathcomp/test_suite/hierarchy_test.v
2019-04-05least common childenCyril Cohen
2019-04-04no output on success in test_suite/hierarchy_test.v (#323)Cyril Cohen
2019-04-02speedup in hierarchy_test.pyCyril Cohen
2019-04-02identifying missing joinsCyril Cohen
2019-03-07Put documentation and some command line options for hierarchy-diagramKazuhiko Sakaguchi
2019-03-07Use both coercions and canonical projections to generate the diagramKazuhiko Sakaguchi
2019-02-22Reimplement hierarchy-diagram by using coercions between "<module>.type" typesKazuhiko Sakaguchi
2019-02-22Add a tool to draw the hierarchy diagramKazuhiko Sakaguchi
2019-02-05fix etc/utils/packager (#273)Cyril Cohen
2018-04-24replacing my local `git root` by a universal commandCyril Cohen
2018-04-24fix opam packager script + dependenciesCyril Cohen
2017-10-23Remove compatibility with Coq.8.4 (and compatibility hacks that went with it)Cyril Cohen
2017-10-20reproduce github archive locally rather than downloading, much fasterCyril Cohen
2017-10-20improved package generatorCyril Cohen
2017-10-19new script to create opam meta packagesCyril Cohen
- the opam files in the branch where the script is launched should be correct - if not, the second argument to the script should be a branch in which the opam files are correct
2017-09-07adding odd_order to the list of released content for 1.6Cyril Cohen
2016-01-05do not use `sed -i' in ssrcoqdep -- this is not portablePierre-Yves Strub
This prevents compilation of ssreflect on OS-X/*BSD.
2015-12-26packaging ssr 1.6Cyril Cohen
2015-12-12modif packager ":" -> "-"Cyril Cohen
2015-12-118.5 coqdoc does not want _ to be escaped + more .css classesEnrico Tassi
2015-12-10some doc for the doc building utilityEnrico Tassi
2015-07-22opam meta-data +urlCyril Cohen
2015-07-22make the opam package meta dataCyril Cohen
2015-07-21make opam meta-dataCyril Cohen
2015-07-21patch ssrcoqdepCyril Cohen
2015-07-17Updating files + reorganizing everythingCyril Cohen
2015-03-09some work on ssreflect and discreteEnrico Tassi