diff options
| -rw-r--r-- | INSTALL.ide | 20 | ||||
| -rw-r--r-- | Makefile | 28 | ||||
| -rw-r--r-- | config/Makefile.template | 3 | ||||
| -rwxr-xr-x | configure | 24 | ||||
| -rw-r--r-- | library/lib.ml | 4 |
5 files changed, 62 insertions, 17 deletions
diff --git a/INSTALL.ide b/INSTALL.ide index f3a0c868c..56bbbb0a7 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -52,16 +52,24 @@ INSTALLATION You must have write access to the OCaml standard library path. If this fails read lablgtk2/README. -2) Go into your Coq source directory and then : +2) Go into your Coq source directory and, as usual, configure with: + + ./configure + + This should detect the ability of making CoqIde. + Then compile with + + make world + + and install with + + make install - make ide - In case you are upgrading from an old version you may need to run make clean-ide -3) You may now run bin/coqide.opt or bin/coqide.byte. - If your coq install is not local, use - make install-ide +3) You may now run bin/coqide + NOTES There are three configuration files located in your $(HOME) dir. @@ -336,7 +336,7 @@ COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) \ coqbinaries:: ${COQBINARIES} -world: coqbinaries states theories contrib tools +world: coqbinaries states theories contrib tools coqide coqlight: coqbinaries states theories-light tools @@ -380,7 +380,7 @@ beforedepend:: scripts/tolink.ml COQIDEBYTE=bin/coqide.byte$(EXE) COQIDEOPT=bin/coqide.opt$(EXE) -COQIDE=bin/coqide.$(BEST)$(EXE) +COQIDE=bin/coqide$(EXE) COQIDECMO=ide/utils/okey.cmo ide/utils/uoptions.cmo \ ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmo \ @@ -402,7 +402,13 @@ beforedepend:: ide/utf8_convert.ml FULLIDELIB=$(FULLCOQLIB)/ide IDEFILES=ide/coq.png ide/.coqide-gtk2rc ide/FAQ -ide: $(COQIDEBYTE) $(COQIDE) states +coqide: coqide-$(HASCOQIDE) +coqide-no: +coqide-byte: $(COQIDEBYTE) $(COQIDE) +coqide-opt: $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE) + +ide: coqide-$(HASCOQIDE) states + clean-ide: rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT) @@ -413,6 +419,9 @@ $(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) $(COQIDECMX) $(COQIDEBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) $(COQIDECMO) $(COQMKTOP) -g -ide -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@ +$(COQIDE): + cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE) + ide/%.cmo: ide/%.ml $(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $< @@ -871,18 +880,19 @@ install-opt: cp $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR) cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE) -install-binaries: +install-binaries: install-ide-$(HASCOQIDE) $(MKDIR) $(FULLBINDIR) cp $(COQDEP) $(GALLINA) $(COQMAKEFILE) $(COQTEX) $(COQINTERFACE) $(COQVO2XML) $(FULLBINDIR) -install-ide: install-ide-$(BEST) - cd $(FULLBINDIR); ln -sf coqide.$(BEST)$(EXE) coqide$(EXE) +install-ide-no: -install-ide-byte: +install-ide-byte: cp $(COQIDEBYTE) $(FULLBINDIR) + cd $(FULLBINDIR); ln -sf coqide.byte$(EXE) coqide$(EXE) -install-ide-opt: install-ide-byte - cp $(COQIDEOPT) $(FULLBINDIR) +install-ide-opt: + cp $(COQIDEBYTE) $(COQIDEOPT) $(FULLBINDIR) + cd $(FULLBINDIR); ln -sf coqide.opt$(EXE) coqide$(EXE) LIBFILES=$(INITVO) $(TACTICSVO) $(THEORIESVO) $(CONTRIBVO) LIBFILESLIGHT=$(INITVO) $(THEORIESLIGHTVO) diff --git a/config/Makefile.template b/config/Makefile.template index bd7bd09d3..a4242ae0e 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -94,5 +94,8 @@ STRIP=STRIPCOMMAND # Options for reals (all/basic) REALS=REALSOPT +# CoqIde (no/byte/opt) +HASCOQIDE=COQIDEOPT + # make or sed are bogus and believe lines not terminating by a return # are inexistent @@ -39,6 +39,7 @@ emacs_spec=no reals_opt=no reals=all arch_spec=no +coqide_spec=no COQTOP=`pwd` @@ -92,6 +93,9 @@ while : ; do -reals|--reals) reals_opt=yes reals=$2 shift;; + -coqide|--coqide) coqide_spec=yes + COQIDE=$2 + shift;; -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;; -debug|--debug) coq_debug_flag=-g;; -profile|--profile) coq_profile_flag=-p;; @@ -310,7 +314,23 @@ case $OS in *) CAMLP4LIB=${CAMLLIB}/camlp4 esac - + +# lablgtk2 and CoqIDE + +if test $coqide_spec == "no"; then +if test -x ${CAMLLIB}/lablgtk2; then + if grep -q -w convert_with_fallback ${CAMLLIB}/lablgtk2/glib.mli; then + COQIDE=byte; + fi + # native threads + if test -f ${CAMLLIB}/threads/threads.cmxa; then + COQIDE=opt + fi +else + COQIDE=no +fi +fi + # Tell on windows if ocaml understands cygwin or windows path formats "$CAMLC" -o config/giveostype config/giveostype.ml @@ -346,6 +366,7 @@ echo " Reals theory : All" else echo " Reals theory : Basic" fi +echo " CoqIde : $COQIDE" echo "" echo " Paths for true installation:" @@ -389,6 +410,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|NATIVECAMLC|$nativecamlc|" \ -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \ -e "s|REALSOPT|$reals|" \ + -e "s|COQIDEOPT|$COQIDE|" \ $COQTOP/config/Makefile.template > $COQTOP/config/Makefile chmod a-w $COQTOP/config/Makefile diff --git a/library/lib.ml b/library/lib.ml index 985d9efba..a4d6aaa22 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -441,7 +441,9 @@ let reset_name (loc,id) = let is_mod_node = function | OpenedModule _ | OpenedModtype _ | OpenedSection _ - | ClosedSection _ -> true | _ -> false + | ClosedSection _ -> true + (* | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" *) + | _ -> false (* Reset on a module or section name in order to bypass constants with the same name *) |