aboutsummaryrefslogtreecommitdiff
path: root/configure
AgeCommit message (Collapse)Author
2017-06-23Merge PR#729: Fixing an inconsistency between configure and configure.mlMaxime Dénès
2017-06-04configure: avoid deprecated warningsPierre Letouzey
2017-06-04Fixing an inconsistency between configure and configure.ml.Hugo Herbelin
The shell script configure was assuming the existence of option -camldir which was removed in 333d41a9.
2013-12-20configure.ml: our configure script is now written in ML :-)Pierre Letouzey
configure is now just a minimal wrapper around the new configure.ml. This configure.ml is runned with the same ocaml used during compilation, and starts with a #load "unix.cma". For now, this new configure script is meant to be 99% compatible with the old one. Known incompatibilities : the --foo option format (with two --) isn't supported anymore, use -foo options instead. Let me know if you encounter any other changes. Internals: - We use our own "run" command (based on Unix.create_process) to avoid relying on some specific shell (/bin/sh or cmd.exe). - We should have far less issues with filename quoting under windows since we almost never rely on (cygwin) shell anymore. This remains to be fully tested, though. - dev/ocamldebug-coq is slightly different now, to ease its generation
2013-12-17Fix make install after 3e972b3ff8e532be233f70567c87512324c99b4ePierre Boutillier
Attempt to adapt .el files too. doc/refman/RefMan-uti.tex has still to be fixed.
2013-11-23configure: typo in my last commitPierre Letouzey
2013-11-22configure: improve last fixPierre Letouzey
Let's avoid the "if a=$(cmd ...)" since: - unless being a shell expert, it's not obvious it's testing the exit code of cmd. - it's quite fragile, if you pipe cmd into a cmd2 you'll lose the exit code of cmd. Instead, we test the emptiness of the variable content afterwards
2013-11-21configure: CAML_LD_LIBRARY_PATH is enriched, not overwrittenPierre Letouzey
Keeping the earlier content of this variable is crucial for opam (at least). Thanks to François Bobot and Thomas Refis for this one...
2013-11-21configure: fix some issues with last commitPierre Letouzey
- after piping with | tr -d, an exit code was lost - suspicious use of " " inside a larger " ", we use ' ' now instead
2013-11-21Fix various \r issues with windowsJason Gross
Also add a 2 in an error message (it's gSourceView2, not gSourceView). This closes bugs 3150, 3151, 3152, and 3153.
2013-11-03Asks camlp5 binary in path its locationpboutill
before looking in CAMLLIB/camlp5 folder Patch by Thomas Braibant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17045 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-03configure stript allows make v4.00pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17042 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-02* configure: Remove trailing space.regisgia
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16753 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Misc changes around coqtop.ml :letouzey
- Revised Coqtop.parse_args in a cleaner and lighter style - Improved error message in case of argument parse failure: * tell which option is expecting a related argument * in case of unknown options, warn about them all at once * do not hide the previous error messages by filling the screen with usage(). Instead, suggest the use of --help. - Specialized boolean config field Coq_config.arch_is_win32 - Faster Envars.coqlib, which is back to (unit->string), and just access Flags.coqlib. Caveat: it must be initialized once via Envars.set_coqlib - Avoid keeping an opened channel to the "revision" file - Direct load of theories/init/prelude.vo, no detour via Loadpath Beware : ./configure must be runned after this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16726 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Change in vo format : digest aren't Marshalled anymoreletouzey
Since digests are strings (of size 16), we just dump them now in vo files (cf. Digest.output) instead of using Marshal on them : this is cleaner and saves a few bytes. Increased VOMAGIC to clearly identify this change in the format. Please rerun ./configure after this commit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16722 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-24New -no-native-compiler flag for configure, globally disabling the nativemdenes
compiler (implemented on Matthieu's request). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16240 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22Revert "remove -rectypes except for term.ml"mdenes
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
2012-11-12Add an option -nodoc to configure, same (but shorter) than -with-doc noletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15962 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Cygwin gcc do not accept -mno-cygwin anymorepboutill
As far as I understand, the standard gcc in cygwin is not able anymore to build non cygwin executable. There is instead a special package with a special gcc that compiles executable that can be used out of cygwin. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15907 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Taking into account that ocamlfind might find a package w/o the filesherbelin
needed for compiling being present. Do the check by hand. Incidentally improved reporting messages. Also check gSourceview.cmi rather than gSourceview.mli for better guess that lablgtk sourceview bindings are there (I've seen installations where gSourceview.mli was here but not gSourceview.cmi). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15901 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06Turn mltop.ml4 into a regular ocaml fileletouzey
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
2012-10-06remove -rectypes except for term.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-05Repair the configure after Hugo's last "repair" ;-)letouzey
Ok, I wasn't aware of the funny behavior of cd in presence of $CDPATH. But the last "repair" was worse, trying to write into non-existing file theories/config/coq_config.ml Things should be better now: * no more Coq_config.theories_dirs at all, since it was completely unused :-) * concerning Coq_config.plugins_dirs, we list them without any "cd" into plugins, hence keeping the "plugins/" part in their paths, and adapt accordingly the only use (!) of plugins_dirs, in coq_makefile Please run ./configure again after upgrading to this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15860 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-04Repaired configure damaged in r15748 for those bash users which haveherbelin
CDPATH variable set. Indeed, command cd is verbose when CDPATH is set, what would introduce garbage in the generated file config/coq_config.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15855 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-04Suggest to use clean rather than archclean before recompiling.herbelin
For instance, generated files depend on whether configuration is done with dynlink or not and they should be cleaned. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15854 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-17MacOS integration uses lablgtkosx >= 1.1pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15814 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-05A few fixes in configure file:herbelin
- Fixing parsing of option -custom - More precise documentation of which option expects an argument - Deprecation of obviously obsolete -emacs option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15773 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23No need anymore to refer to COQLIB in ocamldebug-coqletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15751 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23Configure + Makefile : simplification when -localletouzey
When local=true: - "make install" is now a no-op - In configure, no need hence to fill the various variables about installation (BINDIR, COQLIBINSTALL, MANDIR, DOCDIR, EMACSLIB). This avoids many references to absolute location of the coq sources (which may contain blanks or other strange chars in win32). - For the moment, we keep CONFIGDIR and DATADIR, used when launching coqide from inside the build directory. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15749 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
2012-08-23configure: no more need for ocamlmktopletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15747 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23Simpler configure: gcc via ocamlc, no ranlib (done by ocamlmklib)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15745 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23Port from 8.4 branch some build fixes concerning win32 :letouzey
r15722: - CAMLBIN was cygwin-specific, leading to issues with coqmktop - A missing Filename.quote on the temp file used in coqmktop - Try to shorten the cmdline passed to Sys.command in coqmktop: way too many includes were passed to coqmktop -boot r15724: Coqmktop: the +compiler-libs for ocaml4 is back r15725: Coqmktop: better detection of ocaml 4 and above r15739: ocamlbuild : a missing include for camlp4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15744 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-10Bug 2861 : ocamlopt but no lablgtk2.cmxa problempboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15721 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-07configure: two minor fixes for win32letouzey
* ocamlc -version may end with a \r in win32 (fix #2849) * $COQSRC may initially be cygwin-specific and hence rejected by ocaml. For the moment, an ad-hoc fix is to remove the problematic $COQSRC, and mark the -src option as incompatible with win32... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15696 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12Coq should compile with Ocaml4 and/or lablgtk installed with ocamlfindpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15603 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-23configure: camlp4 is now tried when camlp5 isn't foundletouzey
* When both camlp4 and camlp5 are installed, camlp5 is used by default, except when -usecamlp4 flag is given to ./configure. * Otherwise, ./configure pick automatically the available camlpX git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15349 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-23configure: add support of MinGW Win32 environment (fix #2526)letouzey
* Since MinGW/Msys doesn't provide a cygpath utility, we emulate it via an ocaml script tools/mingwpath.ml * Avoid the crazy sed portions for backslash escaping, instead use a more robust ocaml script tools/escape_string.ml based on String.escaped * No more config/Makefile.template + sed on it, but rather a "cat << EOF > ..." as for config/coq_config.ml * Normally, support of Cygwin should be preserved, as well as mingw32 cross-compilation from linux (cf. myocamlbuild.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15348 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-16Coqide: make some paths win32-compliantletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15332 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-15Makefile: Really avoid locales in $(DATE)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15326 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-11Tentative and very experminental support for typerex. Enabled withaspiwack
./configure -typerex . It causes (non-fatal) errors when compiling files without a .mli (the problem seems to have something to do with the flag -intf-suffix .cmi). In practice, most typerex functionalities don't work well because typerex fails its lookup into files compiled with -rectypes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15302 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-27Configure asks for lablgtk >= 2.12 with gtksourceview2pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15255 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-27Coqide MacOS integration refreshpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15254 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-13Browser documentation & CharSet under Windowspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15157 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-12lib directory is cut in 2 cma.pboutill
- 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
2012-02-20- changing minimal version for OCaml: Coq uses Filename.dirsep that is ↵notin
available from OCaml 3.11.2 (see bug #2707) - fixing outdated address for Coq Club git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14987 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-16Bug 2676: ./configure --prefix shoudn't ask for a config directory.pboutill
I am not really happy of /etc/xdg/coq ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14906 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-23Configure: the backslashes in win32 paths should be escapedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14848 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18./configure & freedesktoppboutill
1/ man dir is now prefix/share/man and not prefix/man git diff! 2/ a data dir option for coqide extra data. 3/ typo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14821 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21coqide default pref files are by default in /etc/xdg/coq/pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14715 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:07:08 +0000