Commit eadc1a98 authored by Armaël Guéneau's avatar Armaël Guéneau

Update opam file and try to make install/uninstall rules more robust

parent 22442a35
......@@ -15,6 +15,9 @@ PREFIX ?= $(DEFAULT_PREFIX)
BINDIR ?= $(PREFIX)/bin
LIBDIR ?= $(PREFIX)/lib/cfml
COQ_WHERE ?= $(shell $(COQBIN)coqc -where)
COQ_CONTRIB := $(COQ_WHERE)/user-contrib
##############################################################################
# Targets.
......@@ -26,9 +29,7 @@ coqlib:
generator:
rm -f generator/cfml_config.ml
sed -e 's|@@PREFIX@@|$(PREFIX)|' \
-e 's|@@BINDIR@@|$(BINDIR)|' \
-e 's|@@LIBDIR@@|$(LIBDIR)|' \
sed -e 's|@@LIBDIR@@|$(LIBDIR)|' \
generator/cfml_config.ml.in > generator/cfml_config.ml
$(MAKE) -C generator
......@@ -58,13 +59,6 @@ clean:
##############################################################################
# Installation.
# If ARTHUR is defined, create a symbolic link from Coq's user-contrib
# directory to this directory (cfml). Otherwise, perform a copy.
# TEMPORARY, this is TODO
COQ_WHERE := $(shell $(COQBIN)coqc -where)
COQ_CONTRIB := $(COQ_WHERE)/user-contrib
# As install depends on all, the file generator/cfml_config.ml is regenerated
# when `make install` is run; this ensures LIBDIR cannot be inconsistent.
......@@ -102,7 +96,7 @@ uninstall:
rm -f $(BINDIR)/cfmlc
# rm -f $(BINDIR)/cfml_cmj
rm -rf $(LIBDIR)
rm -rf $(DOCDIR)
# rm -rf $(DOCDIR)
rm -rf $(COQ_CONTRIB)/CFML
reinstall: uninstall
......
......@@ -4,17 +4,27 @@ maintainer: "armael.gueneau@inria.fr"
authors: [
"Arthur Charguéraud <arthur.chargueraud@inria.fr>"
]
synopsis: "A tool for proving OCaml programs in Separation Logic"
homepage: "https://gitlab.inria.fr/charguer/cfml"
bug-reports: "https://gitlab.inria.fr/charguer/cfml/issues"
license: "CeCILL-B"
dev-repo: "https://gitlab.inria.fr/charguer/cfml.git"
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [make "uninstall"]
install: [
make "install"
"BINDIR=%{_:bin}%" "LIBDIR=%{_:lib}%"
"COQ_WHERE=%{coq:lib}%"
]
remove: [
make "uninstall"
"BINDIR=%{_:bin}%" "LIBDIR=%{_:lib}%"
"COQ_WHERE=%{coq:lib}%"
]
depends: [
"ocaml" {>= "4.03.0"}
"ocamlbuild" {build}
"pprint"
"base-bytes"
"coq" {>= "8.6"}
"coq-tlc" {>= "20171206"}
"coq-tlc" {>= "20181116"}
]
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment