aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure
Commit message (Collapse)AuthorAge
* configure.ml: our configure script is now written in ML :-)Gravatar Pierre Letouzey2013-12-20
| | | | | | | | | | | | | | | | | | 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
* 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.
* configure: typo in my last commitGravatar Pierre Letouzey2013-11-23
|
* configure: improve last fixGravatar Pierre Letouzey2013-11-22
| | | | | | | | | | 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
* configure: CAML_LD_LIBRARY_PATH is enriched, not overwrittenGravatar Pierre Letouzey2013-11-21
| | | | | | | Keeping the earlier content of this variable is crucial for opam (at least). Thanks to François Bobot and Thomas Refis for this one...
* configure: fix some issues with last commitGravatar Pierre Letouzey2013-11-21
| | | | | - after piping with | tr -d, an exit code was lost - suspicious use of " " inside a larger " ", we use ' ' now instead
* Fix various \r issues with windowsGravatar Jason Gross2013-11-21
| | | | | | Also add a 2 in an error message (it's gSourceView2, not gSourceView). This closes bugs 3150, 3151, 3152, and 3153.
* Asks camlp5 binary in path its locationGravatar pboutill2013-11-03
| | | | | | | | 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
* configure stript allows make v4.00Gravatar pboutill2013-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17042 85f007b7-540e-0410-9357-904b9bb8a0f7
* * configure: Remove trailing space.Gravatar regisgia2013-09-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16753 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
| | | | | | | | | | | | | | | | | | | - 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
* Change in vo format : digest aren't Marshalled anymoreGravatar letouzey2013-08-22
| | | | | | | | | | | 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
* New -no-native-compiler flag for configure, globally disabling the nativeGravatar mdenes2013-02-24
| | | | | | | | compiler (implemented on Matthieu's request). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16240 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
* Add an option -nodoc to configure, same (but shorter) than -with-doc noGravatar letouzey2012-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15962 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cygwin gcc do not accept -mno-cygwin anymoreGravatar pboutill2012-10-17
| | | | | | | | 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
* Taking into account that ocamlfind might find a package w/o the filesGravatar herbelin2012-10-17
| | | | | | | | | | 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
* 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
* 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
* Repair the configure after Hugo's last "repair" ;-)Gravatar letouzey2012-10-05
| | | | | | | | | | | | | | | | | | 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
* Repaired configure damaged in r15748 for those bash users which haveGravatar herbelin2012-10-04
| | | | | | | 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
* Suggest to use clean rather than archclean before recompiling.Gravatar herbelin2012-10-04
| | | | | | | 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
* 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
* A few fixes in configure file:Gravatar herbelin2012-09-05
| | | | | | | | - 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
* No need anymore to refer to COQLIB in ocamldebug-coqGravatar letouzey2012-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15751 85f007b7-540e-0410-9357-904b9bb8a0f7
* Configure + Makefile : simplification when -localGravatar letouzey2012-08-23
| | | | | | | | | | | | | | | 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
* configure: get rid of the -src option and of ${COQSRC}Gravatar letouzey2012-08-23
| | | | | | | | | 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
* configure: no more need for ocamlmktopGravatar letouzey2012-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15747 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simpler configure: gcc via ocamlc, no ranlib (done by ocamlmklib)Gravatar letouzey2012-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15745 85f007b7-540e-0410-9357-904b9bb8a0f7
* Port from 8.4 branch some build fixes concerning win32 :Gravatar letouzey2012-08-23
| | | | | | | | | | | | | | 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
* Bug 2861 : ocamlopt but no lablgtk2.cmxa problemGravatar pboutill2012-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15721 85f007b7-540e-0410-9357-904b9bb8a0f7
* configure: two minor fixes for win32Gravatar letouzey2012-08-07
| | | | | | | | | | * 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
* Coq should compile with Ocaml4 and/or lablgtk installed with ocamlfindGravatar pboutill2012-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15603 85f007b7-540e-0410-9357-904b9bb8a0f7
* configure: camlp4 is now tried when camlp5 isn't foundGravatar letouzey2012-05-23
| | | | | | | | | * 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
* configure: add support of MinGW Win32 environment (fix #2526)Gravatar letouzey2012-05-23
| | | | | | | | | | | | | | * 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
* Coqide: make some paths win32-compliantGravatar letouzey2012-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15332 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: Really avoid locales in $(DATE)Gravatar letouzey2012-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15326 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative and very experminental support for typerex. Enabled withGravatar aspiwack2012-05-11
| | | | | | | | | | | | ./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
* Configure asks for lablgtk >= 2.12 with gtksourceview2Gravatar pboutill2012-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15255 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide MacOS integration refreshGravatar pboutill2012-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15254 85f007b7-540e-0410-9357-904b9bb8a0f7
* Browser documentation & CharSet under WindowsGravatar pboutill2012-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15157 85f007b7-540e-0410-9357-904b9bb8a0f7
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
| | | | | | | | | | | | | | | - 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
* - changing minimal version for OCaml: Coq uses Filename.dirsep that is ↵Gravatar notin2012-02-20
| | | | | | | | 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
* Bug 2676: ./configure --prefix shoudn't ask for a config directory.Gravatar pboutill2012-01-16
| | | | | | 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
* Configure: the backslashes in win32 paths should be escapedGravatar letouzey2011-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14848 85f007b7-540e-0410-9357-904b9bb8a0f7
* ./configure & freedesktopGravatar pboutill2011-12-18
| | | | | | | | 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
* coqide default pref files are by default in /etc/xdg/coq/Gravatar pboutill2011-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Patch to support (a priori) all versions of make 3.xx >= 3.81Gravatar herbelin2011-10-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14557 85f007b7-540e-0410-9357-904b9bb8a0f7
* In Coq_config: get rid of coqsrc and make coqlib optionalGravatar glondu2011-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I assume that once Coq is installed in non-local mode and run from its installed path, sources are no longer available. The coqsrc variable doesn't make any sense, then, and its intended value can always be inferred from Sys.executable_name. Moving it to Envars.coqroot. Make coqlib optional. Currently, it is set to None only in -local mode or with ocamlbuild. When set to None, -local layout is assumed (binaries in ./bin, library in .). The behaviour should not be changed when an explicit coqlib has been given to ./configure. This commit should make it possible to run a Coq compiled with -local from anywhere (no hard-coded absolute path embedded in the executables, intermediary step to bug #2565). It WILL BREAK settings re-using source trees after installation in non-local mode (are there actual use cases for that?). Hard-coded absolute paths still remain: - in the build system, so the need to re-run ./configure after moving the source tree is still expected for now; - in coqrunbyteflags, I think we are limited by ocaml itself; - docdir. All absolute paths should be removed, ultimately. As a side-effect, simplify computing of Envars.coqbin. I don't see any good reason to keep it as a function. Disclaimers: - initialization of Sys.executable_name is not consistent across all architectures; relying so much on it might trigger bugs. I'm pretty sure something will explode if one adds arbitrary symlinks on top of that; - ocamlbuild stuff not tested. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14500 85f007b7-540e-0410-9357-904b9bb8a0f7
* default install location under cygwin is the unix defaultGravatar pboutill2011-07-07
| | | | | | apply patch of bug 668. At last... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14266 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 11:16:27 +0000