aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
AgeCommit message (Collapse)Author
2015-03-04Introducing MMaps, a modernized FMaps.Pierre Letouzey
NB: this is work-in-progress, there is currently only one provided implementation (MMapWeakList). In the same spirit as MSets w.r.t FSets, the main difference between MMaps and former FMaps is the use of a new version of OrderedType (see Orders.v instead of obsolete OrderedType.v). We also try to benefit more from recent notions such as Proper. For most function specifications, the style has changed : we now use equations over "find" instead of "MapsTo" predicates, whenever possible (cf. Maps in Compcert for a source of inspiration). Former specs are now derived in FMapFacts, so this is mostly a matter of taste. Two changes inspired by the current Maps of OCaml: - "elements" is now "bindings" - "map2" is now "merge" (and its function argument also receives a key). We now use a maximal implicit argument for "empty".
2015-02-27Adding a new folder corresponding to the low-level part of the pretyperPierre-Marie Pédrot
together with the tactic monad. The move is not complete yet, because some file candidates for this directory have almost useless dependencies in other ones that should not be moved.
2015-02-16Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error), - uniformly expecting paths in Unix format and warning otherwise.
2015-02-16Using home-made ocamllibdep rather than coqdep_boot.Hugo Herbelin
2015-02-14Makefile: in byte we can always dynlinkEnrico Tassi
2015-02-12Revert "Using same code for browsing physical directories in coqtop and coqdep."Hugo Herbelin
(Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
2015-02-12Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error).
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2015-01-06Fix some documentation typos.Guillaume Melquiond
2014-12-19Install .v and .glob files tooEnrico Tassi
PIDE based user interfaces use glob files and source files to implement hyperlinks
2014-10-31STM: reorganize code and file namesEnrico Tassi
- proofworkertop to deal with proof tasks - tacworkertop to deal with par: tactics - queryworkertop to deal with queries (next commit)
2014-10-09No need anymore for referring to xml directory in MLINCLUDES.Hugo Herbelin
2014-09-08Removing the documentation of the XML plugin.Pierre-Marie Pédrot
2014-09-08Removing the XML plugin.Pierre-Marie Pédrot
Left a README, just in case someone will discover the remnants of it decades from now.
2014-09-04Make CoqIDE compile with windows (Closes: 3573)Enrico Tassi
CoqIDE seems to work, but for random pauses that make you think of a thread deadlock, but then, after a few seconds, things make progress again. This happens only seldom on my virtual machine.
2014-09-02coqworkmgrEnrico Tassi
2014-08-26Configure.ml creates metadata to annotate MacOS binariesPierre Boutillier
2014-08-05STM: new "par:" goal selector, like "all:" but in parallelEnrico Tassi
par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2).
2014-07-24Forgot to add a Universes.v.tex as a target.Matthieu Sozeau
2014-07-24fixup fakeide test-suitePierre Boutillier
2014-07-22A makefile rule to build bin/CoqIDE_$VERSION.app macOS bundlePierre Boutillier
The created bundle contains only coqide and gtk (no coqtop, no stdlib)
2014-06-25all coqide specific files moved into ide/Enrico Tassi
lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/
2014-06-25cut toploop(s) out of coqtop: now they are loaded dynamicallyEnrico Tassi
User interface writers can drop a footop.cmxs in $(COQLIB)/toploop/ and pass -toploop footop to customize the coq main loop. A toploop must set Coqtop.toploop_init and Coqtop.toploop_run to functions respectively initializing the toploop (and parsing toploop specific arguments) and running the main loop itself. For backward compatibility -ideslave and -async-proofs worker do set the toploop to coqidetop and stmworkertop respectively.
2014-05-05Fix install target in Makefile after 6acf543800fe176ca7d47ef7165ebc14588efb6f.Maxime Dénès
Should decrease the noise level in the bench.
2014-04-25Adding a stm/ folder, as asked during last workgroup. It was essentially movingPierre-Marie Pédrot
files around. A bunch of files from lib/ that were only used in the STM were moved, as well as part of toplevel/ related to the STM.
2014-03-24Revert "Makefile: the initial build of grammar.cma is now directory-driven"Pierre Letouzey
This reverts commit f694544d016b085b3cd10007b9f7716ae2c3b022. This commit was wrong, since (at least) the highparsing part depends on the toplevel directory. I still didn't had time to fix that, so in the meantime let's revert it.
2014-03-07Compiling coqc in "tools" target.Pierre-Marie Pédrot
2014-03-02Makefile: the initial build of grammar.cma is now directory-drivenPierre Letouzey
In last commit, we used grep to decide whether a .ml4 could be compiled during the initial phase of not. Instead, we now rely on a simpler directory dichotomy: - config lib kernel library pretyping interp parsing grammar are considered initial (and shouldn't contain grammar-dependent .ml4), see $(GRAMSRCDIRS) in Makefile.common - the grammar-dependent .ml4 could be in any other directories Currently, they are in: tactics toplevel plugins/*
2014-02-24Fix coqide build under MacOSPierre Boutillier
2014-01-26Spawn: managed processesEnrico Tassi
The Spawn and Spawned modules factor the operation of spawning a process. Both synchronous and asynchronous channels are supported. Both threaded and glib like main loop models are supported. Still, not all combinations are truly tested not equipped with a decent API: only async + glib and sync + thread are, since these are the models we use for coqide<->coqtop and coqtop<->worker respectively.
2014-01-05refman: fist stab at Asynchronous ProofsEnrico Tassi
2013-12-16A few fixes to the build system (mostly for ocamlbuild)Pierre Letouzey
* vars.mli was mentionning Term instead of Constr, leading to a dep cycle * Having a file named toplevel/toplevel.ml isn't a good idea when we also have a toplevel/toplevel.mllib that ought to produce a toplevel.cma. We rename toplevel.ml into Coqloop.ml * Extra cleanup of toplevel.mllib : - Ppextra isn't anywhere around (?!) - Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway - Vernacexpr is a .mli and shouldn't appear in an .mllib * During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml) * A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread for coqchk).
2013-12-04Documentation of the Derive plugin.Arnaud Spiwack
I put it in a new chapter of the Addendum of the manual. Which is meant to be dedicated to plugins with short documentation.
2013-12-04Derive plugin.Arnaud Spiwack
A small plugin to support program deriving (à la Richard Bird) in Coq. It's fairly simple: Require Coq.Derive.Derive. Derive f From g Upto eq As h. Produces a goal (actually two, but the first one is automatically shelved): |- eq g ?42 And closing the proof produces two definitions: f is instantiated with the value of ?42 (it's always transparent). And h is instantiated with the content of the proof (it is transparent or opaque depending on whether the proof was closed with Defined or Qed).
2013-11-29First stab at documenting Canonical StructuresEnrico Tassi
2013-09-06Moving Searchstack to CStack, and normalizing names a bit.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Searchable stack data structuregareuselesinge
It is like Stack but one can search without popping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16670 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-06New module Xml_printer (dual to Xml_parser)gareuselesinge
Code for printing XML moved from xml_utils.ml to xml_printer.ml and improved to generate less garbage using Buffer.t systematically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16480 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-18coqc and coqmktop migrated in tools/, get rid of scripts/ subdirletouzey
No need to place these binaries apart, and anyway they aren't (shell) scripts since ages. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16432 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Coqmktop: dynlink is now mandatory due to Maxime's native-compilerletouzey
Some cleanup btw, for instance Dynlink.init is deprecated since at least ocaml 3.11 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16419 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-10Tiny fix of r16049pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16055 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-29Allow running coq-tex in win32 (fix #2921)letouzey
Yes, it seems that < and > and even 2>&1 are legal under windows :-) Btw, the only function using streams has been rewritten, so coq_tex is now a standard .ml file, not a .ml4 anymore (beware during upgrade!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15938 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Makefiles: Only -I required dirs (config, lib, ide) when compiling coqidepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15887 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
kernel on CAMLP4/5 structures, and consequently should also erase such structures from vo files. This modification requires some code duplication, mainly while reimplementing our own location data type. This is chiefly visible in the ml4 files, where CAMLP4/5 locations must be manually converted to our locations with an explicit (!@) cast operator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-15Port rewrites of tactic documentation from branch 8.4.gmelquio
This encompasses commits r15183, r15190, r15243, r15262, r15276, r15277, r15278, r15337. The merge did not go without troubles, but hopefully none of the changes were lost in process. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15806 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-12Coqide uses Glib to get the XDG_DATA/CONFIG_HOME/DIRSpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15793 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23No more states/initial.coq, instead coqtop now requires Prelude.voletouzey
For starting a bare coqtop, the recommended option is now "-noinit" that skips the load of Prelude.vo. Option "-nois" is kept for compatibility, it is now an alias to "-noinit". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23No more coqtop.opt, produce directly a coqtop binaryletouzey
We now always produce two binaries, coqtop and coqtop.byte : - If ocamlopt is available, coqtop is directly what used to be coqtop.opt, no more symlinks needed. - Otherwise, coqtop is a copy of coqtop.byte. The same for coqchk and coqide... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15752 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23configure: get rid of the -src option and of ${COQSRC}letouzey
The -src option was antic and probably broken (many references to source files without the $COQRSC prefix). Instead, it's quite simpler to refer to paths in relative way (and safer in win32 where the base path may include spaces and other horrors). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15748 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:38:20 +0000