Define OCaml Config module in ./configure, ./run script, --version option.

diff --git a/.gitignore b/.gitignore
index bd1d969..e47fc4c 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -18,6 +18,8 @@ config.log
 /config.h.in
 /config.status
 /install-sh
+/run
+/src/config.ml
 /src/goals
 /src/lexer.ml
 /src/parser.conflicts

diff --git a/Makefile.in b/Makefile.in
index eeca209..4a8795c 100644 (file)
--- a/Makefile.in
+++ b/Makefile.in
@@ -27,7 +27,10 @@ stamp-h: config.h.in config.status
        touch $@
 
 Makefile: Makefile.in config.status
-       ./config.status Makefile
+       ./config.status $@
+
+run: run.in config.status
+       ./config.status $@
 
 $(srcdir)/configure: configure.ac aclocal.m4
        cd '$(srcdir)' && autoconf

diff --git a/configure.ac b/configure.ac
index d521660..cef6300 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -52,7 +52,9 @@ AC_CHECK_PROG(MENHIR, [menhir], [menhir], [
 dnl Produce output files.
 AC_CONFIG_HEADERS([config.h])
 AC_CONFIG_FILES([stamp-h], [echo timestamp > stamp-h])
+AC_CONFIG_FILES([run], [chmod +x,-w run])
 AC_CONFIG_FILES([Goalfile Makefile
-                 src/Goalfile src/Makefile])
+                 src/Goalfile src/Makefile
+                 src/config.ml])
 
 AC_OUTPUT

diff --git a/run.in b/run.in
new file mode 100644 (file)
index 0000000..928882d
--- /dev/null
+++ b/run.in
@@ -0,0 +1,43 @@
+#!/usr/bin/env bash
+# Goals local run.
+# Copyright (C) 2019 Richard W.M. Jones
+# Copyright (C) 2019 Red Hat Inc.
+# @configure_input@
+#
+# This program is free software; you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# This program 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.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License along
+# with this program; if not, write to the Free Software Foundation, Inc.,
+# 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+# Use ./run goals ... to run goals from a locally compiled copy.
+
+# Function to intelligently prepend a path to an environment variable.
+# See http://stackoverflow.com/a/9631350
+prepend()
+{
+    eval $1="$2\${$1:+:\$$1}"
+}
+
+# Source and build directories (absolute paths so this works from any
+# directory).
+s="$(cd @abs_srcdir@ && pwd)"
+b="$(cd @abs_builddir@ && pwd)"
+
+# Set PATH to include goals binary.
+prepend PATH "$b/src"
+
+# Set up environment variables to add default flags.
+export GOALS_DATADIR="$b"
+
+# Run the program.
+#echo "$@"
+exec "$@"

diff --git a/src/Makefile.in b/src/Makefile.in
index d3e21fc..29e5382 100644 (file)
--- a/src/Makefile.in
+++ b/src/Makefile.in
@@ -17,6 +17,7 @@
 # 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 
 OBJECTS = \
+       config.cmx \
        utils.cmx \
        ast.cmx \
        parser.cmx \
@@ -65,7 +66,10 @@ depend: .depend
 -include .depend
 
 Makefile: Makefile.in ../config.status
-       ../config.status Makefile
+       ../config.status $@
+
+config.ml: config.ml.in ../config.status
+       ../config.status $@
 
 .PHONY: all clean depend
 

diff --git a/src/config.ml.in b/src/config.ml.in
new file mode 100644 (file)
index 0000000..f26a276
--- /dev/null
+++ b/src/config.ml.in
@@ -0,0 +1,24 @@
+(* Goals config
+ * Copyright (C) 2019 Richard W.M. Jones
+ * Copyright (C) 2019 Red Hat Inc.
+ * @configure_input@
+ *
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 2 of the License, or
+ * (at your option) any later version.
+ *
+ * This program 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.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License along
+ * with this program; if not, write to the Free Software Foundation, Inc.,
+ * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+ *)
+
+let package_name = "@PACKAGE_NAME@"
+let package_version = "@PACKAGE_VERSION@"
+let prefix = "@prefix@"
+let datadir = prefix ^ "/share"

diff --git a/src/config.mli b/src/config.mli
new file mode 100644 (file)
index 0000000..2dbd449
--- /dev/null
+++ b/src/config.mli
@@ -0,0 +1,23 @@
+(* Goals config
+ * Copyright (C) 2019 Richard W.M. Jones
+ * Copyright (C) 2019 Red Hat Inc.
+ *
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 2 of the License, or
+ * (at your option) any later version.
+ *
+ * This program 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.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License along
+ * with this program; if not, write to the Free Software Foundation, Inc.,
+ * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+ *)
+
+val package_name : string
+val package_version : string
+val prefix : string
+val datadir : string

diff --git a/src/main.ml b/src/main.ml
index 7565b10..c23b70a 100644 (file)
--- a/src/main.ml
+++ b/src/main.ml
@@ -35,7 +35,20 @@ For detailed help see goals(1).
 
 Options:"
 
+let print_version () =
+  printf "%s %s\n" Config.package_name Config.package_version;
+  exit 0
+
 let main () =
+  (* Get stdlib directory. *)
+  let datadir =
+    try Sys.getenv "GOALS_DATADIR" with Not_found -> Config.datadir in
+  let stdlibdir = datadir // "stdlib" in
+  let prelude_gl = stdlibdir // "prelude.gl" in
+  if not (is_directory stdlibdir) || not (Sys.file_exists prelude_gl) then
+    failwithf "%s: cannot find the standard library directory, expected %s.  If the standard library directory is in a non-standard location then set GOALS_DATADIR.  If you can trying to run goals from the build directory then use ‘./run goals ...’"
+      Sys.executable_name stdlibdir;
+
   (* Command line arguments. *)
   let args = ref [] in
   let directory = ref "." in
@@ -50,6 +63,10 @@ let main () =
                    "filename Set name of Goalfile";
     "--file",      Arg.Set_string filename,
                    "filename Set name of Goalfile";
+    "-V",          Arg.Unit print_version,
+                   " Print version and exit";
+    "--version",   Arg.Unit print_version,
+                   " Print version and exit";
   ] in
   let argspec = Arg.align argspec in
   let anon_fun s = args := s :: !args in

diff --git a/src/utils.ml b/src/utils.ml
index 235167d..c495675 100644 (file)
--- a/src/utils.ml
+++ b/src/utils.ml
@@ -21,6 +21,9 @@ open Printf
 
 let failwithf fs = ksprintf failwith fs
 
+let (//) = Filename.concat
+let is_directory d = try Sys.is_directory d with Sys_error _ -> false
+
 (* From OCaml 4.08 sources.  We can remove this when we can
  * depend on min OCaml 4.08.
  *)

diff --git a/src/utils.mli b/src/utils.mli
index cb99fad..e3981cd 100644 (file)
--- a/src/utils.mli
+++ b/src/utils.mli
@@ -20,6 +20,12 @@
 val failwithf : ('a, unit, string, 'b) format4 -> 'a
 (** Like [failwith] but supports printf-like arguments. *)
 
+val (//) : string -> string -> string
+(** The {!Filename.concat} function. *)
+
+val is_directory : string -> bool
+(** Return true iff parameter is a directory. *)
+
 val filter_map : ('a -> 'b option) -> 'a list -> 'b list
 (** [filter_map f l] applies [f] to every element of [l], filters
     out the [None] elements and returns the list of the arguments of