Skip to content

Commit

Permalink
Replace libdir by a dedicated variable, and add support for DESTDIR.
Browse files Browse the repository at this point in the history
  • Loading branch information
silene committed Dec 17, 2020
1 parent 39a2b8d commit 6a1eda0
Show file tree
Hide file tree
Showing 3 changed files with 15 additions and 19 deletions.
10 changes: 5 additions & 5 deletions INSTALL.md
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,8 @@ to set the Coq compiler command. The configure script defaults to `coqc`.
Similarly, `COQDEP` can be used to specify the location of `coqdep`. The
`COQBIN` environment variable can be used to set both variables at once.

The option `--libdir=DIR` can be set to the directory where the compiled
library files should be installed by `./remake install`. By default, the
target directory is `` `$COQC -where`/user-contrib/Flocq ``.

The files are compiled at a logical location starting with `Flocq`.
The library files are compiled at the logical location `Flocq`. The
`COQUSERCONTRIB` environment variable can be used to override the
physical location where the `Flocq` directory containing these files will
be installed by `./remake install`. By default, the target directory is
`` `$COQC -where`/user-contrib ``.
13 changes: 6 additions & 7 deletions Remakefile.in
Original file line number Diff line number Diff line change
Expand Up @@ -127,13 +127,12 @@ public: deps.png deps.map html/index.html
cp -r html deps.png public/

install:
prefix=@prefix@
exec_prefix=@exec_prefix@
mkdir -p @libdir@
for d in Core Calc Prop IEEE754 Pff; do mkdir -p @libdir@/$d; done
for f in $(OBJS); do cp $f @libdir@/${f#src/}; done
for f in $(FILES); do cp src/$f @libdir@/$f; done
( cd src && find . -type d -name ".coq-native" -exec cp -RT "{}" "@libdir@/{}" \; )
dir="${DESTDIR}@COQUSERCONTRIB@/Flocq"
mkdir -p $dir
for d in Core Calc Prop IEEE754 Pff; do mkdir -p $dir/$d; done
for f in $(OBJS); do cp $f $dir/${f#src/}; done
for f in $(FILES); do cp src/$f $dir/$f; done
( cd src && find . -type d -name ".coq-native" -exec cp -RT "{}" "$dir/{}" \; )

EXTRA_DIST = \
configure
Expand Down
11 changes: 4 additions & 7 deletions configure.in
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,6 @@ if test "$ac_init_help" = "long"; then
fi
m4_divert_pop(99)

m4_divert_push([HELP_ENABLE])
Fine tuning of the installation directory:
AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where`/user-contrib/Flocq@:>@])
m4_divert_pop([HELP_ENABLE])

AC_PROG_CXX

AC_DEFUN([AX_VERSION_GE], [AS_VERSION_COMPARE([$1],[$2],[$4],[$3],[$3])])
Expand Down Expand Up @@ -70,8 +65,10 @@ AC_MSG_RESULT([$COQDOC])

AC_ARG_VAR(COQEXTRAFLAGS, [extra flags passed to Coq compiler [empty]])

if test "$libdir" = '${exec_prefix}/lib'; then
libdir="`$COQC -where | tr -d '\r' | tr '\\\\' '/'`/user-contrib/Flocq"
AC_ARG_VAR(COQUSERCONTRIB, [installation directory [`$COQC -where`/user-contrib]])

if test -z "$COQUSERCONTRIB"; then
COQUSERCONTRIB="`$COQC -where | tr -d '\r' | tr '\\\\' '/'`/user-contrib"
fi

AC_MSG_NOTICE([building remake...])
Expand Down

0 comments on commit 6a1eda0

Please sign in to comment.