Commit b3d1d542 authored by Andrei Paskevich's avatar Andrei Paskevich

rework configure:

- no more version.sh, use config.ml.in and version.tex.in instead
- dynlink compatibility is moved to config.ml
- comment out unused sections in Makefile
- provide the explicit --enable-ide option
- provide the explicit --enable-plugins option
- require at least Ocaml 3.10
- remove *-yes and *-no targets from Makefile,
  use ifeq() instead
parent 077da58b
This diff is collapsed.
......@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
open Why
let print_context _ fmt _ = Format.fprintf fmt "helloworld@\n"
let transform_context = Register.identity
......
......@@ -17,6 +17,7 @@
(* *)
(**************************************************************************)
open Why
open Term
open Theory
open Env
......@@ -31,7 +32,7 @@ let make_rt_rf env =
try
find_theory env prelude array
with TheoryNotFound (l,s) ->
Format.eprintf "The theory %a is unknown" print_theorynotfound (l,s);
Format.eprintf "The theory %s is unknown" s;
exit 1 in
let store = (ns_find_ls array.th_export store).ls_name in
let select = (ns_find_ls array.th_export select).ls_name in
......
......@@ -46,7 +46,6 @@
# OCAMLYACC "ocamlyac"
# OCAMLLIB the path to the ocaml standard library
# OCAMLVERSION the ocaml version number
# LABLGTK2 "yes" is available, "no" otherwise
# OCAMLWEB "ocamlweb" (not mandatory)
......@@ -56,11 +55,27 @@ AC_INIT(src/)
# verbosemake feature
AC_ARG_ENABLE(verbosemake,[ --enable-verbosemake verbose makefile commands],VERBOSEMAKE=yes,VERBOSEMAKE=no)
if test "$VERBOSEMAKE" = yes ; then
AC_MSG_RESULT(Make will be verbose.)
fi
AC_ARG_ENABLE(verbose-make,
[ --enable-verbose-make verbose makefile commands],,
enable_verbose_make=no)
# IDE feature
AC_ARG_ENABLE(ide,
[ --enable-ide enable Why IDE],,
enable_ide=yes)
# dynlink feature
AC_ARG_ENABLE(plugins,
[ --enable-plugins enable Why3 plugins],,
enable_plugins=yes)
# Coq plugin feature
AC_ARG_ENABLE(coq-support,
[ --enable-coq-support enable Coq support],,
enable_coq_support=yes)
# Check for arch/OS
......@@ -89,30 +104,18 @@ fi
OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
echo "ocaml version is $OCAMLVERSION"
case $OCAMLVERSION in
0.*|1.*|2.00|3.00*|3.01*|3.02*|3.03*|3.04*|3.05*|3.06*|3.07*)
AC_MSG_ERROR(You need Objective 3.08 or later);;
3.08.2)
FORPACK=""
OCAMLV=3082;;
3.08*)
FORPACK=""
OCAMLV=308;;
*)
FORPACK="-for-pack Graph";;
esac
#Dynlink is native?
case $OCAMLVERSION in
3.08*|3.09*|3.10*)
DYNLINK="Dynlink_"
enable_dynlink=no;;
#Dynlink_ is used for compatibility in /src/util/dynlink_compat.ml.in
*)
DYNLINK="Dynlink"
enable_dynlink=yes
case "$OCAMLVERSION" in
0.*|1.*|2.*|3.0*)
AC_MSG_ERROR(You need Objective Caml 3.10 or later);;
3.10*)
enable_plugins=no;;
esac
if test "$enable_plugins" = "yes" ; then
DYNLINK="Dynlink"
else
DYNLINK="Dynlink_"
fi
# Ocaml library path
# old way: OCAMLLIB=`$OCAMLC -v | tail -1 | cut -f 4 -d ' ' | tr -d '\\r'`
......@@ -203,31 +206,29 @@ else
fi
# checking for lablgtk2
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtk.cma,LABLGTK2=yes,LABLGTK2=no)
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtksourceview2.cma,LABLGTK2=yes,LABLGTK2=no)
# AC_CHECK_PROG(LABLGTK2,lablgtk2,yes,no) not always available (Win32)
if test "$LABLGTK2" = yes ; then
if test "$enable_ide" = yes ; then
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtk.cma,,enable_ide=no)
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtksourceview2.cma,,enable_ide=no)
fi
dnl AC_CHECK_PROG(enable_ide,lablgtk2,yes,no) not always available (Win32)
if test "$enable_ide" = yes ; then
INCLUDEGTK2="-I +lablgtk2"
fi
AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true)
dnl AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true)
# Coq
AC_ARG_ENABLE(coq-support,
[ --enable-coq-support enable the coq support)[default=yes]],,
enable_coq_support=yes)
if test "$enable_coq_support" = no; then
COQ=no
enable_coq_support=no
AC_MSG_WARN(coq support disabled)
else
AC_CHECK_PROG(COQC,coqc,coqc,no)
if test "$COQC" = no ; then
COQ=no
enable_coq_support=no
AC_MSG_WARN(Cannot find coqc.)
else
COQ=yes
enable_coq_support=yes
AC_CHECK_PROG(COQDEP,coqdep,coqdep,true)
if test "$COQDEP" = true ; then
AC_MSG_ERROR(Cannot find coqdep.)
......@@ -237,21 +238,29 @@ else
COQVERSION=`$COQC -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
case $COQVERSION in
8.*|trunk)
8.*|trunk)
AC_MSG_RESULT($COQVERSION);;
*)
COQ=no
*)
enable_coq_support=no
AC_MSG_WARN(You need Coq 8.x or later; Coq discarded);;
esac
fi
fi
#Viewer for ps and pdf
AC_CHECK_PROGS(PSVIEWER,gv evince)
AC_CHECK_PROGS(PDFVIEWER,xpdf acroread evince)
dnl AC_CHECK_PROGS(PSVIEWER,gv evince)
dnl AC_CHECK_PROGS(PDFVIEWER,xpdf acroread evince)
. ./Version
BUILDDATE="$(date)"
# substitutions to perform
AC_SUBST(VERBOSEMAKE)
AC_SUBST(VERSION)
AC_SUBST(BUILDDATE)
AC_SUBST(enable_verbose_make)
AC_SUBST(EXE)
AC_SUBST(STRIP)
AC_SUBST(CPULIMIT)
......@@ -266,28 +275,27 @@ AC_SUBST(OCAMLBEST)
AC_SUBST(OCAMLVERSION)
AC_SUBST(OCAMLV)
AC_SUBST(OCAMLLIB)
AC_SUBST(OCAMLGRAPHLIB)
AC_SUBST(LABLGTK2)
dnl AC_SUBST(OCAMLGRAPHLIB)
AC_SUBST(enable_ide)
AC_SUBST(INCLUDEGTK2)
AC_SUBST(OCAMLWEB)
dnl AC_SUBST(OCAMLWEB)
AC_SUBST(DYNLINK)
AC_SUBST(FORPACK)
dnl AC_SUBST(FORPACK)
AC_SUBST(COQ)
AC_SUBST(enable_coq_support)
AC_SUBST(COQC)
AC_SUBST(COQDEP)
AC_SUBST(COQLIB)
AC_SUBST(COQVER)
AC_SUBST(COQVERSION)
AC_SUBST(PSVIEWER)
AC_SUBST(PDFVIEWER)
dnl AC_SUBST(PSVIEWER)
dnl AC_SUBST(PDFVIEWER)
# Finally create the Makefile from Makefile.in
dnl AC_OUTPUT(Makefile)
AC_CONFIG_FILES(Makefile bench/bench src/driver/dynlink_compat.ml)
AC_CONFIG_FILES(Makefile src/config.ml doc/version.tex)
AC_OUTPUT
chmod a-w Makefile
chmod a-w bench/bench
chmod a+x bench/bench
chmod a-w Makefile src/config.ml doc/version.tex
# Summary
......@@ -296,11 +304,11 @@ echo " Summary"
echo "-----------------------------------------"
echo "OCaml version : $OCAMLVERSION"
echo "OCaml library path : $OCAMLLIB"
echo "Verbose make : $VERBOSEMAKE"
echo "Why plugin enabled : $enable_dynlink"
echo "Why IDE : $LABLGTK2"
echo "Coq support : $COQ"
if test "$COQ" = "yes" ; then
echo " Version : $COQVER ($COQVERSION)"
echo "Verbose make : $enable_verbose_make"
echo "Why IDE : $enable_ide"
echo "Why plugins : $enable_plugins"
echo "Coq support : $enable_coq_support"
if test "$enable_coq_support" = "yes" ; then
echo " Version : $COQVERSION"
echo " Lib : $COQLIB"
fi
\newcommand{\whyversion}{@VERSION@}
......@@ -16,21 +16,25 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
# 19 "src/driver/dynlink_compat.ml.in"
module Dynlink_ =
struct
let is_native = true (* Dumb value *)
let loadfile_private _ = assert false (* Shouldn't be used *)
let why_version = "@VERSION@"
let why_builddate = "@BUILDDATE@"
let coq_version = "@COQVERSION@"
module Dynlink_ = struct
let is_native_not_defined = true
let is_native = true
let loadfile_private _ = assert false
type error
exception Error of error
let error_message : error -> string = fun _ -> assert false
let error_message _ = (assert false : string)
end
module Dynlink =
struct
let is_native_not_defined = "@DYNLINK@" = "_Dynlink"
include @DYNLINK@
end
module Dynlink = struct
let is_native_not_defined = false
include @DYNLINK@
end
......@@ -182,16 +182,12 @@ let () =
"Pervasives";"Format";"List";"Sys";"Unix"]
*)
open Dynlink_compat
let load_plugin dir (byte,nat) =
if Dynlink.is_native_not_defined then
errorm
"Why has been compiled with a version of caml which doesn't allow\
native dynlink. So Why chooses to refuse plugin.";
let file = if Dynlink.is_native then nat else byte in
if Config.Dynlink.is_native_not_defined then
errorm "Plugins are not supported";
let file = if Config.Dynlink.is_native then nat else byte in
let file = Filename.concat dir file in
Dynlink.loadfile_private file
Config.Dynlink.loadfile_private file
let load_file file =
let c = open_in file in
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
module Dynlink :
sig
val is_native_not_defined : bool
val is_native : bool
val loadfile_private : string -> unit
type error
exception Error of error
val error_message : error -> string
end
......@@ -188,8 +188,8 @@ let rec report fmt = function
fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_short
| Driver.Error e ->
Driver.report fmt e
| Dynlink_compat.Dynlink.Error e ->
fprintf fmt "Dynlink : %s" (Dynlink_compat.Dynlink.error_message e)
| Config.Dynlink.Error e ->
fprintf fmt "Dynlink : %s" (Config.Dynlink.error_message e)
| e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
let print_th_namespace fmt th =
......
#!/bin/sh
# Note: the BINDIR variable is a free variable
# Note: the LIBDIR variable is a free variable
# Note: the COQVER variable is a free variable
# Note: the mkdirs are needed for the Ocamlbuild Makefile.
. ./Version
# Why
WHYVF=src/config.ml
mkdir -p src
echo "let coqversion = \"$COQVER\"" > $WHYVF
echo "let version = \"$VERSION\"" >> $WHYVF
echo "let date = \""`date`"\"" >> $WHYVF
echo "let bindir = \"$BINDIR\"" >> $WHYVF
echo "let libdir = \"$LIBDIR/why\"" >> $WHYVF
echo "let datadir = \"$DATADIR/why\"" >> $WHYVF
# Doc
DOCF=doc/version.tex
mkdir -p doc
printf '\\newcommand{\\whyversion}{'$VERSION'}\n' > $DOCF
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