From: Richard W.M. Jones Date: Sat, 28 Dec 2019 19:54:50 +0000 (+0000) Subject: Define OCaml Config module in ./configure, ./run script, --version option. X-Git-Tag: v'0.2'~122 X-Git-Url: http://git.annexia.org/?a=commitdiff_plain;h=315ceff80b09b76959a067fa2f3288f22d2e55da;p=goals.git Define OCaml Config module in ./configure, ./run script, --version option. --- diff --git a/.gitignore b/.gitignore index bd1d969..e47fc4c 100644 --- 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 --- 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 --- 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 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 --- 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 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 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 --- 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 --- 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 --- 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