Commit c38fc2fa authored by Armaël Guéneau's avatar Armaël Guéneau

Store install locations in generator/cfml_config.ml and use these to find stdlib's cmj

parent 9ac5f32d
......@@ -4,6 +4,18 @@ CFML := $(shell pwd)
include Makefile.common
##############################################################################
# Installation destinations.
DEFAULT_PREFIX := $(shell opam config var prefix)
ifeq ($(DEFAULT_PREFIX),)
DEFAULT_PREFIX := /usr/local
endif
PREFIX ?= $(DEFAULT_PREFIX)
BINDIR ?= $(PREFIX)/bin
LIBDIR ?= $(PREFIX)/lib/cfml
##############################################################################
# Targets.
......@@ -14,6 +26,11 @@ coqlib:
$(MAKE) -C lib/coq proof
generator:
rm -f generator/cfml_config.ml
sed -e 's|@@PREFIX@@|$(PREFIX)|' \
-e 's|@@BINDIR@@|$(BINDIR)|' \
-e 's|@@LIBDIR@@|$(LIBDIR)|' \
generator/cfml_config.ml.in > generator/cfml_config.ml
$(MAKE) -C generator
examples: all
......@@ -36,6 +53,7 @@ clean:
$(MAKE) -C lib/coq $@
$(MAKE) -C lib/stdlib $@
$(MAKE) -C generator $@
rm -f generator/cfml_config.ml
rm -f $(DOC)
##############################################################################
......
let libdir = "@@LIBDIR@@"
......@@ -26,6 +26,8 @@ let outputfile = ref None
(*#########################################################################*)
let (^/) = Filename.concat
let spec =
Arg.align [
("-I", Arg.String (fun i -> Clflags.include_dirs := i::!Clflags.include_dirs),
......@@ -40,6 +42,8 @@ let spec =
("-only_normalize", Arg.Set only_normalize, " only generate the .cmj file, and attempt normalization, not the .v file");
("-debug", Arg.Set is_tracing, " trace the various steps");
("-width", Arg.Set_int Print_coq.width, " set pretty-printing width for the .v file");
("-where", Arg.Unit (fun () -> print_endline Cfml_config.libdir; exit 0),
"print CFML's library files location and exit");
]
(*
......@@ -65,10 +69,9 @@ let _ =
*)
Clflags.strict_sequence := true;
(* todo: improve the path to mystdlib *)
let gen_dir = Filename.dirname Sys.argv.(0) in
if not !no_mystd_include
then Clflags.include_dirs := (gen_dir ^ "/../lib/ocaml")::!Clflags.include_dirs;
if not !no_mystd_include then
Clflags.include_dirs :=
(Cfml_config.libdir ^/ "stdlib") :: !Clflags.include_dirs;
trace "1) parsing of command line";
if List.length !files <> 1 then
......
......@@ -14,6 +14,7 @@ let no_mystd_include = ref false
(*#########################################################################*)
let (^/) = Filename.concat
let _ =
Settings.configure();
......@@ -25,24 +26,23 @@ let _ =
"includes a directory where to look for interface files");
("-rectypes", Arg.Set Clflags.recursive_types, "activates recursive types");
("-nostdlib", Arg.Set no_mystd_include, "do not include standard library");
("-nopervasives", Arg.Set Clflags.nopervasives, "do not include standard pervasives file") ]
("-nopervasives", Arg.Set Clflags.nopervasives, "do not include standard pervasives file");
("-where", Arg.Unit (fun () -> print_endline Cfml_config.libdir; exit 0),
"print CFML's library files location and exit");
]
(fun f -> files := f::!files)
("usage: [-I dir] [..other options..] file.mli");
Clflags.strict_sequence := true;
if not !no_mystd_include then
Clflags.include_dirs :=
(Cfml_config.libdir ^/ "stdlib") :: !Clflags.include_dirs;
(* todo: improve the path to mystdlib *)
let gen_dir = Filename.dirname Sys.argv.(0) in
if not !no_mystd_include
then Clflags.include_dirs := (gen_dir ^ "/camllib")::!Clflags.include_dirs;
if List.length !files <> 1
if List.length !files <> 1
then failwith "Expects one argument: the filename of the MLI file";
let sourcefile = List.hd !files in
let extension = String.sub sourcefile (String.length sourcefile - 3) 3 in
if extension <> "mli"
if not (Filename.check_suffix sourcefile ".mli")
then failwith "Extension should be .mli";
let _basename = String.sub sourcefile 0 (String.length sourcefile - 4) in
let output_prefix = Misc.chop_extension_if_any sourcefile (* _basename ^ ".cmj"*) in
let output_prefix = Misc.chop_extension_if_any sourcefile in
typecheck_interface_file ppf sourcefile output_prefix;
Printf.printf "Wrote %s.cmj\n" output_prefix
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