From a48b05d35f0646322e8178ff10f8ed7af3e739aa Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Sun, 5 Jan 2020 21:23:59 +0000 Subject: [PATCH] Standardize running code in a single function, include prelude.sh. --- src/cmdline.ml | 5 +++-- src/cmdline.mli | 5 ++++- src/eval.ml | 55 ++++++++++++++++++++++++++++++++----------------------- src/eval.mli | 8 +++----- src/main.ml | 2 +- src/run.ml | 8 ++------ stdlib/prelude.gl | 14 +++----------- stdlib/prelude.sh | 28 ++++++++++++++++++++++++++++ 8 files changed, 76 insertions(+), 49 deletions(-) create mode 100644 stdlib/prelude.sh diff --git a/src/cmdline.ml b/src/cmdline.ml index b155298..f98e0a8 100644 --- a/src/cmdline.ml +++ b/src/cmdline.ml @@ -43,9 +43,10 @@ let print_version () = let datadir = try Sys.getenv "GOALS_DATADIR" with Not_found -> Config.datadir let stdlibdir = datadir // "stdlib" -let prelude_file = stdlibdir // "prelude.gl" +let prelude_gl_file = stdlibdir // "prelude.gl" +let prelude_sh_file = stdlibdir // "prelude.sh" let () = - if not (is_directory stdlibdir) || not (Sys.file_exists prelude_file) then + if not (is_directory stdlibdir) || not (Sys.file_exists prelude_gl_file) 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 diff --git a/src/cmdline.mli b/src/cmdline.mli index cb6265d..aed4e8b 100644 --- a/src/cmdline.mli +++ b/src/cmdline.mli @@ -20,9 +20,12 @@ val stdlibdir : string (** Get the stdlib directory. *) -val prelude_file : string +val prelude_gl_file : string (** Get the absolute path of the prelude.gl file. *) +val prelude_sh_file : string +(** Get the absolute path of the prelude.sh file. *) + val input_file : string (** Get the name of the input Goalfile. This is an absolute path. *) diff --git a/src/eval.ml b/src/eval.ml index c2d6551..4496319 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -142,6 +142,33 @@ and expr_to_shell_string env = function failwithf "%a: cannot use tactic in shell expansion" Ast.string_loc loc +and run_code ?(quiet = false) env loc code = + let code = to_shell_script env loc code in + let code = + "source " ^ Filename.quote Cmdline.prelude_sh_file ^ "\n" ^ + "set -e\n" ^ + (if not quiet then "set -x\n" else "") ^ + "\n" ^ + code in + + let chan = Unix.open_process_in code in + let b = Buffer.create 1024 in + (try + while true do + Buffer.add_string b (input_line chan); + Buffer.add_char b '\n' + done + with End_of_file -> ()); + let st = Unix.close_process_in chan in + let i = + match st with + | Unix.WEXITED i -> i + | Unix.WSIGNALED i -> + failwithf "%a: killed by signal %d" Ast.string_loc loc i + | Unix.WSTOPPED i -> + failwithf "%a: stopped by signal %d" Ast.string_loc loc i in + i, Buffer.contents b + and evaluate_goal_arg env = function | Ast.EVar (loc, name) -> let expr = Ast.getvar env loc name in @@ -208,27 +235,9 @@ and call_function env loc name args (params, code) = (List.length params) (List.length args) in List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in - (* Run the code. *) - let code = to_shell_script env loc code in - let code = "set -e\n" (*^ "set -x\n"*) ^ "\n" ^ code in - - let chan = Unix.open_process_in code in - let b = Buffer.create 1024 in - (try - while true do - Buffer.add_string b (input_line chan); - Buffer.add_char b '\n' - done - with End_of_file -> ()); - let st = Unix.close_process_in chan in - (match st with - | Unix.WEXITED 0 -> () - | Unix.WEXITED i -> - eprintf "*** function ‘%s’ failed with exit code %d\n" name i - | Unix.WSIGNALED i -> - eprintf "*** function ‘%s’ killed by signal %d\n" name i - | Unix.WSTOPPED i -> - eprintf "*** function ‘%s’ stopped by signal %d\n" name i + let r, b = run_code env loc code in + if r <> 0 then ( + eprintf "*** function ‘%s’ failed with exit code %d\n" name r; + exit 1 ); - - Parse.parse_expr (sprintf "function:%s" name) (Buffer.contents b) + Parse.parse_expr (sprintf "function:%s" name) b diff --git a/src/eval.mli b/src/eval.mli index 40a4de8..2a86601 100644 --- a/src/eval.mli +++ b/src/eval.mli @@ -27,11 +27,9 @@ val to_constant : Ast.env -> Ast.expr -> Ast.constant raises [Failure _]. *) val substitute : Ast.env -> Ast.loc -> Ast.substs -> string -(** Similar to {!substitute} except this is used where we will - pass the result immediately to the shell to execute. Variables - are substituted with shell quoted strings. Raises [Failure _] - on error. *) -val to_shell_script : Ast.env -> Ast.loc -> Ast.substs -> string +(** Run a code section. Returns the exit code and the output printed + by the script. Raises [Failure _] on error. *) +val run_code : ?quiet:bool -> Ast.env -> Ast.loc -> Ast.substs -> int * string (** Evaluate a goal argument. This substitutes any variables found, and recursively calls functions. *) diff --git a/src/main.ml b/src/main.ml index 6421aa8..df4fb43 100644 --- a/src/main.ml +++ b/src/main.ml @@ -31,7 +31,7 @@ let main () = (* Parse the prelude. *) let env = if Cmdline.use_prelude then - Parse.parse_goalfile Ast.Env.empty Cmdline.prelude_file + Parse.parse_goalfile Ast.Env.empty Cmdline.prelude_gl_file else Ast.Env.empty in diff --git a/src/run.ml b/src/run.ml index d8cabb9..6d14f9d 100644 --- a/src/run.ml +++ b/src/run.ml @@ -132,9 +132,7 @@ and run_goal env loc name args (params, patterns, deps, code) extra_deps = match deps with | [] -> env | d :: _ -> Ast.Env.add "^" d env in - let code = Eval.to_shell_script env loc code in - let code = "set -e\nset -x\n\n" ^ code in - let r = Sys.command code in + let r, _ = Eval.run_code env loc code in if r <> 0 then ( eprintf "*** goal ‘%s’ failed with exit code %d\n" name r; exit 1 @@ -193,9 +191,7 @@ and needs_rebuild env loc deps extra_deps pattern = match deps with | [] -> env | d :: _ -> Ast.Env.add "^" d env in - let code = Eval.to_shell_script env loc code in - let code = "set -e\n" (*^ "set -x\n"*) ^ "\n" ^ code in - let r = Sys.command code in + let r, _ = Eval.run_code ~quiet:true env loc code in if r = 99 (* means "needs rebuild" *) then true else if r = 0 (* means "doesn't need rebuild" *) then false else ( diff --git a/stdlib/prelude.gl b/stdlib/prelude.gl index f9fa642..fdb23e9 100644 --- a/stdlib/prelude.gl +++ b/stdlib/prelude.gl @@ -40,29 +40,21 @@ tactic *exists (filename) = { #---------------------------------------------------------------------- # Text functions. -# Sort + uniq a list. -function sort (xs) = { - # XXX Quoting - echo '[' - for f in %xs; do echo "$f"; done | - sort -u | - sed 's/.*/"&",/' - echo ']' -} + #---------------------------------------------------------------------- # File functions. # Expand a wildcard into a list of filenames. function wildcard (wc) = { - # XXX Quoting shopt -s nullglob # Note that the substitution is quoted by goals, so to expand # it we must assign it to a variable and then use it unquoted. wc=%wc echo '[' for f in $wc; do - echo "\"$f\"," + quoted_string "$f" + echo ',' done echo ']' } diff --git a/stdlib/prelude.sh b/stdlib/prelude.sh new file mode 100644 index 0000000..5b42f4e --- /dev/null +++ b/stdlib/prelude.sh @@ -0,0 +1,28 @@ +# Goals stdlib shell prelude. +# Copyright (C) 2020 Richard W.M. Jones +# Copyright (C) 2020 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. + +# This file is included in all shell scripts, and is used to define +# various common functions. + +# This should be used to print the single parameter as a quoted string +# suitable for consuming in a goal expression. +function quoted_string () +{ + # XXX This doesn't actually do quoting XXX + echo "\"$1\"" +} -- 1.8.3.1