diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-16 21:16:05 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-16 21:16:05 +0000 |
| commit | 22739b29af99bc06c1d63003853650df5de47f8f (patch) | |
| tree | 4a75d36747473c6456d16de3edec310b93291874 | |
| parent | a3f08185150e8ae0ce00e142edfcf7009f126e93 (diff) | |
Install csdpcert with libraries
csdpcert is not meant to be called directly by the user
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11327 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 12 | ||||
| -rw-r--r-- | Makefile.common | 2 | ||||
| -rw-r--r-- | contrib/micromega/coq_micromega.ml | 4 |
3 files changed, 11 insertions, 7 deletions
diff --git a/Makefile.build b/Makefile.build index d4e021d43..0475865c0 100644 --- a/Makefile.build +++ b/Makefile.build @@ -361,11 +361,11 @@ contrib/contrib.cmxa: $(CONTRIB:.cmo=.cmx) ########################################################################### ifeq ($(BEST),opt) -bin/csdpcert$(EXE): $(CSDPCERTCMX) +contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMX) $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa -o $@ $(CSDPCERTCMX) else -bin/csdpcert$(EXE): $(CSDPCERTCMO) +contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMO) $(SHOW)'OCAMLC -o $@' $(HIDE)$(OCAMLC) -custom $(BYTEFLAGS) nums.cma -o $@ $(CSDPCERTCMO) endif @@ -630,12 +630,12 @@ install-binaries:: install-$(BEST) install-tools install-byte:: $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CSDPCERT) $(FULLBINDIR) + $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR) cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE) install-opt:: $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(CSDPCERT) $(FULLBINDIR) + $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR) cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE) install-tools:: @@ -660,6 +660,10 @@ ifeq ($(BEST),opt) $(INSTALLLIB) $(LINKCMX) $(FULLCOQLIB) endif find . -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \; + # csdpcert is not meant to be directly called by the user; + # we install it with libraries + -$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega + $(INSTALLBIN) $(CDSPCERT) $(FULLCOQLIB)/contrib/micromega install-library-light: $(MKDIR) $(FULLCOQLIB) diff --git a/Makefile.common b/Makefile.common index 6b7da1a57..3aacdef73 100644 --- a/Makefile.common +++ b/Makefile.common @@ -46,7 +46,7 @@ COQBINARIES:= $(COQMKTOP) $(COQC) \ endif OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE) -CSDPCERT:=bin/csdpcert$(EXE) +CSDPCERT:=contrib/micromega/csdpcert$(EXE) ########################################################################### # tools diff --git a/contrib/micromega/coq_micromega.ml b/contrib/micromega/coq_micromega.ml index 847ae7baa..890671ab5 100644 --- a/contrib/micromega/coq_micromega.ml +++ b/contrib/micromega/coq_micromega.ml @@ -1294,8 +1294,8 @@ let call_csdpcert provername poly = output_value ch_to (provername,poly : provername * micromega_polys); close_out ch_to; let cmdname = - Filename.concat Coq_config.bindir - ("csdpcert" ^ Coq_config.exec_extension) in + List.fold_left Filename.concat Coq_config.coqlib + ["contrib"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in let c = Sys.command (cmdname ^" "^ tmp_to ^" "^ tmp_from) in (try Sys.remove tmp_to with _ -> ()); if c <> 0 then Util.error ("Failed to call csdp certificate generator"); |