diff --git a/asli.nix b/asli.nix index e7c34f44..843109d6 100644 --- a/asli.nix +++ b/asli.nix @@ -21,7 +21,7 @@ ocamlPackages.buildDunePackage { doCheck = lib.versionAtLeast ocaml.version "4.09"; configurePhase = '' - sed -i 's|`opam config var ott:share`|${pkgs.ott.out + "/share/ott"}|' ./libASL/dune + export ASLI_OTT=${pkgs.ott.out + "/share/ott"} mkdir -p $out/asl cp -rv prelude.asl mra_tools tests $out/asl ''; diff --git a/aslp.nix b/aslp.nix index 08c2bc7d..b72f1110 100644 --- a/aslp.nix +++ b/aslp.nix @@ -11,6 +11,8 @@ ASL_PATH=${asli}/asl cd ${asli}/bin makeBinaryWrapper "$(pwd)/asli" $out/bin/aslp \ + --append-flags --prelude \ + --append-flags $ASL_PATH/prelude.asl \ --append-flags $ASL_PATH/prelude.asl \ --append-flags $ASL_PATH/mra_tools/arch/regs.asl \ --append-flags $ASL_PATH/mra_tools/types.asl \ diff --git a/bin/asli.ml b/bin/asli.ml index 944f4da6..c9906af9 100644 --- a/bin/asli.ml +++ b/bin/asli.ml @@ -19,6 +19,7 @@ module TC = Tcheck module PP = Asl_parser_pp module AST = Asl_ast +let opt_prelude : string ref = ref "prelude.asl" let opt_filenames : string list ref = ref [] let opt_print_version = ref false let opt_verbose = ref false @@ -284,6 +285,7 @@ let options = Arg.align ([ ( "-x", Arg.Set_int opt_debug_level, " Debugging output"); ( "-v", Arg.Set opt_verbose, " Verbose output"); ( "--version", Arg.Set opt_print_version, " Print version"); + ( "--prelude", Arg.Set_string opt_prelude," ASL prelude file (default: ./prelude.asl)"); ] ) let version = "ASL 0.2.0 alpha" @@ -311,7 +313,7 @@ let main () = else begin if !opt_verbose then List.iter print_endline banner; if !opt_verbose then print_endline "\nType :? for help"; - let t = LoadASL.read_file "prelude.asl" true !opt_verbose in + let t = LoadASL.read_file !opt_prelude true !opt_verbose in let ts = List.map (fun filename -> if Utils.endswith filename ".spec" then begin LoadASL.read_spec filename !opt_verbose diff --git a/libASL/dune b/libASL/dune index f0a8b500..8197d9b6 100644 --- a/libASL/dune +++ b/libASL/dune @@ -10,7 +10,7 @@ (progn (run ott -aux_style_rules false -tex_wrap true -quotient_rules false -i asl.ott -o asl_parser_head.mly -o asl_lexer.mll -o asl_ast.ml) (run mv asl_parser_head_pp.ml asl_parser_pp.ml) - (with-stdout-to asl_parser_tail.mly (bash "grep -v '^%%' `opam config var ott:share`/menhir_library_extra.mly")) + (with-stdout-to asl_parser_tail.mly (bash "OTT=${ASLI_OTT:-$(opam config var ott:share)}; grep -v '^%%' $OTT/menhir_library_extra.mly")) (with-stdout-to asl_parser.mly (run cat asl_parser_head.mly asl_parser_tail.mly))))) (library diff --git a/shell.nix b/shell.nix new file mode 100644 index 00000000..ebb7f415 --- /dev/null +++ b/shell.nix @@ -0,0 +1,20 @@ +{ pkgs ? import {} }: +pkgs.mkShell { + packages = [ pkgs.opam pkgs.ocaml pkgs.ott pkgs.ocamlPackages.merlin pkgs.ocamlPackages.ocaml-lsp pkgs.ocamlformat ]; + + inputsFrom = [ pkgs.asli ]; + + shellHook = '' + export DEBUG=1 + export OPAMSWITCH=nix-shell-asli + CAML_LD_PREV=$CAML_LD_LIBRARY_PATH + + opam init --no-setup + opam switch create $OPAMSWITCH ocaml-system + eval $(opam env) + + export ASLI_OTT=${pkgs.ott}/share/ott + + export CAML_LD_LIBRARY_PATH=$CAML_LD_PREV:$CAML_LD_LIBRARY_PATH + ''; +}