aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
Commit message (Collapse)AuthorAge
* Change handling of loadpath and mlpath.Gravatar Guillaume Melquiond2014-04-06
| | | | | | | | | | | | | - Option -I no longer handles loadpath, only mlpath. This is the same behavior as coq_makefile. Option -I-as is unchanged. - Option -R no longer recursively adds to mlpath; only the root directory is added. - user-contrib/ and xdg directories are no longer recursively added to the loadpath. - theories/ and plugins/ are no longer recursively added to the loadpath when option -nois is passed. - All the preconfigured directories are still recursively added to the mlpath though.
* Revert "Makefile: the initial build of grammar.cma is now directory-driven"Gravatar Pierre Letouzey2014-03-24
| | | | | | | | 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.
* make install-coqlight installs DLLCOQRUN and LIBCOQRUNGravatar Pierre Boutillier2014-03-06
|
* Set officially the minimal OCaml requirement to 3.12.1Gravatar Pierre Letouzey2014-03-02
| | | | | | | | | | | | | | | Anyway, a few syntactic features of 3.12 were already used here and there (e.g. local opening via Foo.(...), or the record shortcut { field; ... }). Hence compiling with 3.11 wasn't working anymore. Already take advantage of the following 3.12.1 features : - "module type of ..." in CArray, CList, CString ... - "ocamldep -ml-synonym" : no need anymore to hack the ocamldep output via our coqdep to localize the .ml4 modules :-) The -ml-synonym option (+ various bugfixes) is the reason for asking 3.12.1 directly and not just 3.12.0. After all, if debian stable is providing 3.12.1, then everybody has it ;-)
* Makefile: the initial build of grammar.cma is now directory-drivenGravatar Pierre Letouzey2014-03-02
| | | | | | | | | | | | | 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/*
* Makefile: re-introduce 2 phases to avoid make strange -include'sGravatar Pierre Letouzey2014-02-27
| | | | | | | | | | | | | | | | | | | | | | | | | Yet another revision of the build system. We avoid relying on the awkward include-which-fails-but-works-finally-after-a-retry feature of gnu make. This was working, but was quite hard to understand. Instead, we reuse the idea of two explicit phases (as in 2007 and its stage{1,2,3}), but in a lighter way. The main Makefile calls Makefile.build twice : - first for building grammar.cma (and q_constr.cmo), with a restricted set of .ml4 to consider (see variables BUILDGRAMMAR and ML4BASEFILES). - then on the true target(s) asked by the user (using the special variable MAKECMDGOALS). In pratice, this should change very little to the concrete developper's life, let me know otherwise. A few more messages of make due to the explicit first sub-call, but no more strange "not ready yet" messages... Btw: we should handle correctly now the parallel compilation of multiple targets (e.g. make -jX foo bar). As reported by Pierre B, this was triggering earlier two separate sub-calls to Makefile.build, one for foo, the other for bar, with possibly nasty interactions in case of parallelism. In addition, some cleanup of Makefile.build, removal of useless :: rules, etc etc.
* make coqide-binaries does not build coqtop anymoreGravatar Pierre Boutillier2014-02-24
|
* Fix coqide build under MacOSGravatar Pierre Boutillier2014-02-24
|
* fake_ide: ported to spawnGravatar Enrico Tassi2014-02-10
|
* Coqmktop without Sys.command, changes in ./configure -*byteflags optionsGravatar Pierre Letouzey2014-01-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | NB: Please re-run ./configure after pulling this commit For launching ocamlc/ocamlopt, coqmktop doesn't use Sys.command anymore, but rather CUnix.sys_command, which is based on Unix.create_process. This way, we do not need to bother with the underlying shell (/bin/sh or cmd.exe) and the way arguments are to be quoted :-). Btw, many cleanups of coqmktop. Only difficulty: the -coqrunbyteflags of ./configure is a "meta-option" that collect as a string several sub-options to be given by coqmktop to ocamlc. For instance ./configure -coqrunbyteflags "-dllib -lcoqrun". We need now to parse all these sub-options. To ease that, I've made the following changes to the ./configure options: * The -coqrunbyteflags and its blank-separated argument isn't accepted anymore, and is replaced by a new option -vmbyteflags which expects a comma-separated argument. For instance: ./configure -vmbyteflags "-dllib,-lcoqrun" Btw, on this example, the double-quotes aren't mandatory anymore :-) * The -coqtoolsbyteflags isn't accepted anymore. To the best of my knowledge, nobody ever used it directly (it was internally triggered as a byproduct of the -custom option). The only interest I can think of for this option was to cancel the default use of ocamlc custom-linking on Win32 and MacOS. For that, ./configure now provides a -no-custom option.
* configure.ml fixed wrt Win32 + byte-only + coqideGravatar Enrico Tassi2014-01-26
|
* Goodbye typerex, Hello merlinGravatar Pierre2014-01-09
|
* md5 for MacOSGravatar Pierre2014-01-09
| | | | md5sum check remains not portable.
* Makefile.build: avoid a -ppGravatar Pierre Letouzey2013-12-20
|
* Coqdep always uses / as dir_sepGravatar Pierre Boutillier2013-12-20
|
* Fix make install after 3e972b3ff8e532be233f70567c87512324c99b4eGravatar Pierre Boutillier2013-12-17
| | | | | Attempt to adapt .el files too. doc/refman/RefMan-uti.tex has still to be fixed.
* Do not compile coqide with -threadGravatar Pierre Boutillier2013-12-12
| | | | Coqide compiled with -thread seems to hang for ever at startup under MacOS
* Revert the two last commits. My bad, I messed up git-svn commands...Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16951 85f007b7-540e-0410-9357-904b9bb8a0f7
* Printing heap on every processed sentence.Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16949 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: move cmd_stack to a separate module: DocumentGravatar gareuselesinge2013-10-10
| | | | | | | | The idea is to move the logic related to document handling to a separate module that can be tested by fake_ide too. CoqOps should "only" interface Document with the GtkTextBuffer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16870 85f007b7-540e-0410-9357-904b9bb8a0f7
* fake_ide: speak the new protocolGravatar gareuselesinge2013-10-07
| | | | | | | | | A new syntax for .fake files, allowing multi line phrases and labeled script points (to go back to them). Test 7 fails because of a bug in STM (in a very spaghetti-like script). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16860 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing ocamldebug compilation by adding thread linking.Gravatar ppedrot2013-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16801 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix compilation of coqcheckGravatar gareuselesinge2013-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16716 85f007b7-540e-0410-9357-904b9bb8a0f7
* State Transaction MachineGravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | | | | | | | | | The process_transaction function adds a new edge to the Dag without executing the transaction (when possible). The observe id function runs the transactions necessary to reach to the state id. Transaction being on a merged branch are not executed but stored into a future. The finish function calls observe on the tip of the current branch. Imperative modifications to the environment made by some tactics are now explicitly declared by the tactic and modeled as let-in/beta-redexes at the root of the proof term. An example is the abstract tactic. This is the work described in the Coq Workshop 2012 paper. Coq is compile with thread support from now on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing argument extension. Instead of qualified names, stringGravatar ppedrot2013-06-19
| | | | | | | representing qualified names where interpreted as a whole lowercase ident. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16593 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing the various glob/subst/interp registering functions forGravatar ppedrot2013-06-18
| | | | | | extra argument types and putting them into Genarg. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16586 85f007b7-540e-0410-9357-904b9bb8a0f7
* New module Xml_printer (dual to Xml_parser)Gravatar gareuselesinge2013-05-06
| | | | | | | 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
* Coqide: new feedback mechanism for structured contentGravatar gareuselesinge2013-04-25
| | | | | | | | | | | | | | | | | This amounts to a new type of message called "feedback" and defined in Interface to hold structured data. Coq sends feedback messages asynchronously (they are all fetched, like regular messages, together with the main response to a call) and they are related to a specific sentence by an id. Other changes: - CoqOps pushes the sentence to be processed onto the cmd_stack before processing it and pulls it back if Coq.intep fails, in this way the handler for feedback messages can just look at the cmd_stack to find the offset of the sentence to eventually apply the new Gtk.tag. - The class coqops takes in input a coqtop to set its feedback_handle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16451 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqc and coqmktop migrated in tools/, get rid of scripts/ subdirGravatar letouzey2013-04-18
| | | | | | | 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
* Checker : a md5-based way to ensure checker/values.ml is always in syncGravatar letouzey2013-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16404 85f007b7-540e-0410-9357-904b9bb8a0f7
* votour: a small tool for guided tours of .voGravatar letouzey2013-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16403 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checker: re-sync vo structures after Maxime's commit 16136Gravatar letouzey2013-02-12
| | | | | | | make validate still fails, but that's another issue (#2949) we're still working on... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16198 85f007b7-540e-0410-9357-904b9bb8a0f7
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
| | | | | | | | | | | | | 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
* Revert "remove -rectypes except for term.ml"Gravatar mdenes2013-01-22
| | | | | | | | | | Preparing landing of the native compiler, which requires -rectypes flag. This reverts commit f975575187d0a19e7cc1afc43459a92eeb12b3f1. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16135 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: get rid of threads, use gtk asynchronous i/o insteadGravatar letouzey2012-12-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Threads were only there to handle blocking dialogs with the different coqtops. But programming with threads have drawbacks : complex mutex infrastructure, possible deadlocks, etc. In particular gtk functions are not meant to be called from a thread which isn't the gtk main loop, (unless some gtk mutex have been taken). This seem to pose problem specifically in win32 (and macosx ?), hence the use of the GtkThread.(a)sync hack for scheduling code for execution in the gtk main loop. Instead, we now use the Glib.Io module to install a callback that will be runned when some answer of coqtop is available on the channel. This implies using now a continuation-passing style: for instance, instead of two sequential requests to coqtop, we'll now have the 2nd request inside the callback handling the answer to the 1st request. Remarks: - Also use asynchronous i/o for external commands (editor, coqc, make...). Launching an external editor or browser won't freeze coqide anymore. - Reworked handling of coqtop process, especially when closing them. A responsive coqtop should now hara-kiri immediatly when its input channel is closed. Otherwise we try later a soft kill, then some hard kills if necessary. If nothing work we warns the user. When quitting coqide, all this might induce a small delay (2s at worse). - Be careful now to avoid "long" computations (or blocking i/o) in a coqide function. Experimentally, it seems that loading/saving a .v file is quick enough. If necessary, we could use asynchronous i/o also for writing the .v, but for loading I've no clue. - In the Coqide module, we ensure that the current continuation k will indeed be run at the end thanks to an abstract return type (void = opaque copy of unit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqmktop: missing -I (fix #2851)Gravatar letouzey2012-10-23
| | | | | | | | | | | | The modules used in coqmktop's temporary main file should have their .cmi in the search path, hence a small set of -I is required: lib, toplevel. We do not place their the full list to avoid issues with the win32 command-line length Btw, coqmktop -boot now also builds its list of -I instead of receiving them via its command-line, it's simpler this way... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15926 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide does not need dllcoqrun.soGravatar pboutill2012-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15914 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile.build: CONFIG is now in clibGravatar pboutill2012-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15909 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not install libcoqrun.so if compiled with -customGravatar pboutill2012-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15908 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefiles: Only -I required dirs (config, lib, ide) when compiling coqideGravatar pboutill2012-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15887 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile.build: $(MLINCLUDES) out of $(OPT/BYTEFLAGS)Gravatar pboutill2012-10-15
| | | | | | Allow to erase special $(CHKFLAGS) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15886 85f007b7-540e-0410-9357-904b9bb8a0f7
* Turn mltop.ml4 into a regular ocaml fileGravatar letouzey2012-10-06
| | | | | | | | | | | | | | | | | | The IFDEF's in mltop.ml4 were there to support platforms with a native ocaml compiler but no dynlink.cmxa, a situation that should be pretty rare in the Coq community nowadays (playing with coqtop on ARM, anyone ?). So we now refuse to build a native coqtop unless dynlink.cmxa exists (cf ./configure), and we explain how to create a dummy one if necessary (cf dev/dynlink.ml). This way, we can clean-up mltop.ml, and remove ugly special rules in Makefile and myocamlbuild NB: I checked that this shouldn't have any impact on Coq's debian packages on exotic architectures (arm, mips, ...), since apparently on these architectures no ocamlopt at all are shipped, and coq packages are already byte-only git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15879 85f007b7-540e-0410-9357-904b9bb8a0f7
* no need for camlp4 cma's in coq misc toolsGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15876 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove -rectypes except for term.mlGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile.build: easier compilation with timings infoGravatar letouzey2012-10-04
| | | | | | | | | | | | | | | On a reasonable platform equipped with a /usr/bin/time, a simple "make TIMED=1" should provide you with timings of the .v compilations. If you don't have /usr/bin/time, or prefer a different output format, you can still do a "make TIMECMD='...'". For storing the timings in a spreadsheet, simply do: "make TIMED=1 2> timings.csv" and then import this csv in your favorite office program, with whitespace as separator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15850 85f007b7-540e-0410-9357-904b9bb8a0f7
* New makefile shortcuts miniopt and minibyte for coqtop + pluginsGravatar letouzey2012-10-02
| | | | | | | They are meant to quickly check that all the ml code of coqtop and its plugins is compilable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15841 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a ml-dot option to Makefile to generate dependency graph of core modulesGravatar ppedrot2012-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15832 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid generating ide/coqide_main*.ml as cleartext (except if READABLE_ML4 is ↵Gravatar letouzey2012-09-20
| | | | | | used) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15824 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove broken makefile option NO_RECOMPILE_LIBGravatar letouzey2012-09-20
| | | | | | | | | | | | | | | The idea was to allow rebuilding coqtop without the whole stdlib, but it's not working anymore since the stdlib also depends on plugins .cmxs, hence its compilation will be triggered anyway. Since I've no idea how to restore the old behavior (except via hacking the output of coqdep with more ORDER_ONLY hack), I simply declare this option dead, and remove it for improving clarity. NB: an imperfect workaround is to touch all the .vo after rebuilding coqtop and the plugins... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15823 85f007b7-540e-0410-9357-904b9bb8a0f7
* MacOS integration uses lablgtkosx >= 1.1Gravatar pboutill2012-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15814 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 06:36:18 +0000