aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/envars.ml
Commit message (Collapse)AuthorAge
...
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIde files position is freedesktop compliant.Gravatar pboutill2011-12-18
| | | | | | | Beware, it means that files position is not relative to coqtop position but is given by XDG_DATA_DIRS and XDG_CONFIG_DIRS. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14822 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqrc in the right XDG_CONFIG_HOME/coq folderGravatar pboutill2011-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14696 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add support for XDG_DATA_HOME and XDG_DATA_DIRS.Gravatar pboutill2011-11-20
| | | | | | From Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14692 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
* Choose relative directory over configured directory for coqlib.Gravatar pboutill2011-04-29
| | | | | | | | | This also fixes the bug where Util.error is always called, if coq searches for a relative directory. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14084 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqtop -config returns coq returns coq environments at exection timeGravatar pboutill2011-04-28
| | | | | | It looks like a variables definition part of a Makefile. Names are from coq makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14080 85f007b7-540e-0410-9357-904b9bb8a0f7
* Win32: remove the need for Coq.bat and Coqide.batGravatar letouzey2011-04-21
| | | | | | | | | | | | | | | | This is an adaptation of commit r13750 of branch 8.3 - coqlib is currently computed relatively of Sys.executable_name, hence no need to set it manually - in Win32, better detection of user home dir : in System.ml, if HOME isn't set, we look now for HOMEDRIVE\HOMEPATH, and then for USERPROFILE - concerning PATH, in Win32 we now add coqbin (or the location of coqide) to PATH during the initialization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14041 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add directories in COQPATH to search path.Gravatar herbelin2011-04-14
| | | | | | | | This is to allow users to install plugins when coq is installed system-wide. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14001 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Gestion des espaces dans les noms + guess_coqlib sous WindowsGravatar notin2009-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11921 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix d'un problème lors de l'appel à coqtop avec un chemin relatifGravatar notin2009-02-11
| | | | | | (cherry picked from commit 76796fca17ec7763b1301b0dd22c07ddc92983fc) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11917 85f007b7-540e-0410-9357-904b9bb8a0f7
* Experimental file commited by mistake, sorry.Gravatar herbelin2009-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
| | | | | | | | | | - Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove trailing newlines in outputs of X -whereGravatar glondu2009-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11768 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made the debugger work again:Gravatar herbelin2009-01-02
| | | | | | | | | | | | | | - call to open_process_full from Envars.camlp4lib was apparently disturbing stdin/stdout/stderr and precipitating coqtop.byte death in ocamldebug; renounced to add camlp4 to the ml path (why was it useful?) which was the reason for calling camlp4lib (seems like camlp4lib is now useless), - Envars was needing str.cma which was missing when calling printers.cma; renounced to use str.cma since its only use was for an elementary split function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11734 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
principaux changements sont: - coqtop (et coqc) maintenant insensible aux variables d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les librairies Coq peut être spécifié par l'option -coqlib - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les chemins des exécutables OCaml; en dehors du mode boot, coqmktop cherche les exécutables OCaml dans PATH - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci étant installé en copiant l'architecture des sources (ie lib.cmxa est installé dans COQLIB/lib/lib.cmxa) - coq_makefile prend maintenant 3 paramètres sous forme de variables d'environnement: COQBIN pour dire où trouver les exécutables Coq, CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les chemins vers les librairies sont déduits en utilisant -where Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de simuler les conditions de la vie réelle (Ocaml pas dans le PATH, installation binaire relocalisée, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 18:03:45 +0000