Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Commits on Sep 20, 2012
  1. Remove broken makefile option NO_RECOMPILE_LIB

    letouzey authored
     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
Commits on Aug 23, 2012
  1. No more states/initial.coq, instead coqtop now requires Prelude.vo

    letouzey authored
     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
  2. No more coqtop.opt, produce directly a coqtop binary

    letouzey authored
     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
Commits on May 29, 2012
  1. Makefile: avoid too much exported vars (for win32)

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15366 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Apr 27, 2012
  1. @pirbo

    Configure asks for lablgtk >= 2.12 with gtksourceview2

    pirbo authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15255 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Apr 12, 2012
  1. @pirbo

    make otags only relies on otags

    pirbo authored
    but it requires otags-3.12.2 and and ./configure -usecamlp4
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15147 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. @pirbo

    lib directory is cut in 2 cma.

    pirbo authored
     - Clib that does not depend on camlpX and is made to be shared by all coq
       tools/scripts/...
     - Lib that is Coqtop specific
    
    As a side effect for the build system :
     - Coq_config is in Clib and does not appears in makefiles
     - only the BEST version of coqc and coqmktop is made
     - ocamlbuild build system fails latter but is still broken
    
    (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.)
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jan 17, 2012
  1. Makefile: fix make distclean w.r.t. test-suite

    letouzey authored
     No need for a distclean rule in test-suite, since the root-level distclean
     already launches clean, which launches clean in test-suite, and this one
     does the job
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14915 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Sep 5, 2011
  1. fake_ide: a short program to mimic an ide talking to coqtop -ideslave

    letouzey authored
      This way, we can test each night that coqtop -ideslave handles
      correctly some specific sequences of API calls.
      For the moment, we add a few tests of the backtracking.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14456 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Apr 8, 2011
  1. @pirbo

    Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395

    pirbo authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13976 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jan 25, 2011
  1. Add a test for sorting all universes of stdlib

    glondu authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13797 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Sep 10, 2010
  1. @pirbo

    files introduce in commit 13401 aren't erased anymore by 'make clean'

    pirbo authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13404 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jun 23, 2010
  1. Ajout d'une feuille de style pour les définitions spécifiques à Hevea…

    notin authored
    … + divers corrections sur la génération du manuel de référence.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13186 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jun 2, 2010
  1. Fix test-suite cleaning

    glondu authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13052 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Apr 29, 2010
  1. @pirbo

    "make source-doc" builds documentation of mli in html and pdf at

    pirbo authored
    dev/ocamldoc/
    
    old "make source-doc" that documents ml files and didn't work is now
    "make ml-doc" but still don't work :-)
    
    "make clean" cleans dev/ocamldoc/ properly
    
    wierd? calls of dependency graph generation leave unchanged
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12978 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. Remove the svn-specific $Id$ annotations

    letouzey authored
     - Many of them were broken, some of them after Pierre B's rework
       of mli for ocamldoc, but not only (many bad annotation, many files
       with no svn property about Id, etc)
     - Useless for those of us that work with git-svn (and a fortiori
       in a forthcoming git-only setting)
     - Even in svn, they seem to be of little interest
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 5, 2010
  1. Makefile: some more cleanup

    letouzey authored
     - avoid recomputing CAMLP4DEPS in the %.ml:%.ml4 rule
     - a macro for compiling the tools by the best ocaml compiler
     - use of $(if ...) rather that $ifdef
     - some variables of Makefile.common were not that useful
       (e.g. $(COQCCMX), which is $(COQCCCMO:.cmo=.cmx), used only once)
     - the build of coqc.* should not depend upon coqtop, only its launch
       (or I'm missing something)
     - useless $(CAMLP4EXTENDFLAGS) variable
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12846 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 4, 2010
  1. Makefile: cleanup of comments + a few words about recent changes in d…

    letouzey authored
    …ev/doc/build*.txt
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12840 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. Makefile: no more separate stages

    letouzey authored
     - Instead of the separate stage mechanism, we let make handle the
       build and inclusion of all .d. Some initial calls to camlp4o
       will fail, but make tries again later, and this finally works
       great. These initial error message are made nice to avoid bad
       interaction with M-x next-error
    
     - The only recursive call to a sub-make is Makefile calling Makefile.build
       in which the includes of .d take place. This allows to avoid compiling
       anything for a make clean or make tags
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12839 85f007b7-540e-0410-9357-904b9bb8a0f7
  3. Makefile: cleanup of variables containing lists of files, such as MLF…

    letouzey authored
    …ILES
    
     - We clarify their definition via some custom make function: find, diff...
     - We avoid duplications via some $(sort ...)
     - Some name changes:
        * old $(MLFILES) now corresponds to $(MLSTATICFILES) (but .ml from
          .mly and .mll aren't in it anymore).
        * new $(MLFILES) contains all .ml, either static or generated from
          .mly .mll .ml4 or _mod.ml made out of .mllib
        * $(ML4FILESML) is now $(GENML4FILES)
        ...
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12836 85f007b7-540e-0410-9357-904b9bb8a0f7
  4. Makefile: make devdocclean was not removing *.dep.ps, btw let's remov…

    letouzey authored
    …e *.dep.ps for svn
    
     the syntax for find is sooo intuitive ...
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12835 85f007b7-540e-0410-9357-904b9bb8a0f7
  5. Makefile: the .ml of .ml4 are now produced explicitely (in binary ast…

    letouzey authored
    … form)
    
    - This way, the Makefile.build gets shorter and simplier, with a few nasty
       hacks removed.
     - In particular, we stop creating dummy .ml of .ml4 early "to please ocamldep".
       Instead, we now use ocamldep -modules, and process its output via coqdep_boot.
       This ways, *.cm* of .ml4 are correctly located, even when some .ml files
       aren't generated yet.
     - There is no risk of editing the .ml of a .ml4 by mistake, since it is by
       default in a binary format (cf pr_o.cmo and variable READABLE_ML4).
       M-x next-error still open the right .ml4 at the right location.
     - mltop.byteml is now mltop.ml, while mltop.optml keeps its name
     - .ml of .ml4 are added to .gitignore
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12833 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Feb 26, 2010
  1. Slight reorganisation of make clean, new entry cleankeepvo

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12818 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jan 28, 2010
  1. Remove bashisms

    glondu authored
    As pointed out by Nima Hoda, bash is not installed everywhere... and
    we really don't NEED bash anyway.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12701 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jan 26, 2010
  1. make init + NMake.v/NMake_gen.v

    notin authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12690 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Dec 2, 2009
  1. Remove interface plugin

    glondu authored
    It has moved to the contribs (Sophia-Antipolis/Interface).
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12555 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Sep 28, 2009
  1. Applied patches from BSD/pkgsrc maintainer, so that Coq compiles out-…

    gmelquio authored
    …of-the-box.
    
    - Removed unneeded bashisms. (sh and dash are fine with the current build system.)
    - Removed workaround for camlp4.opt on BSD.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12362 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Sep 21, 2009
  1. Update link to "Recursive Make Considered Harmful"

    glondu authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12349 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Apr 8, 2009
  1. Backport of Eric Le Lay's patch (bug report #2078) from v8.2 branch

    herbelin authored
    (r12063) for smooth compilation/installation under Solaris (/bin/sh ->
    /bin/bash, -or -> -o in find, echo -n -> printf, ! in test rather than
    in if).
    
    
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12065 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Apr 3, 2009
  1. Makefile: ocamlbuild's _build is not traversed by find, and removed b…

    letouzey authored
    …y make clean
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12047 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 31, 2009
  1. Committed patch sent by Samuel Bronson on Mar 14 2009 to take care of

    herbelin authored
    .bzr files (Bazaar management files) in VCS clause (see 12043 in v8.2
    branch).
    
    
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12044 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 26, 2009
  1. clean revision and coqdep_boot, too

    lmamane authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12016 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 20, 2009
  1. Directory 'contrib' renamed into 'plugins', to end confusion with arc…

    letouzey authored
    …hive of user contribs
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 18, 2009
  1. renamed %-mod.ml into %_mod.ml to avoid ocaml warning

    barras authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11994 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Mar 17, 2009
  1. Makefile:clean: rm *-mod.ml

    barras authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11988 85f007b7-540e-0410-9357-904b9bb8a0f7
Something went wrong with that request. Please try again.