diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/TimeFileMaker.py | 3 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 8 |
2 files changed, 10 insertions, 1 deletions
diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index 8564aeff64..854dd25b75 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -2,7 +2,8 @@ from __future__ import with_statement from __future__ import division from __future__ import unicode_literals from __future__ import print_function -import os, sys, re +import sys +import re from io import open # This script parses the output of `make TIMED=1` into a dictionary diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index 62a871aa0e..fa8b771a74 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -127,6 +127,7 @@ module Options = struct let all_opts = [ { enabled = false; cmd = "-debug"; } ; { enabled = false; cmd = "-native_compiler"; } + ; { enabled = true; cmd = "-allow-sprop"; } ] let build_coq_flags () = @@ -235,6 +236,12 @@ let scan_plugins m = let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath ["plugins";f]) Array.(to_list @@ readdir "plugins")) in List.fold_left scan_mlg m dirs +(* This will be removed when we drop support for Make *) +let fix_cmo_cma file = + if String.equal Filename.(extension file) ".cmo" + then replace_ext ~file ~newext:".cma" + else file + (* Process .vfiles.d and generate a skeleton for the dune file *) let parse_coqdep_line l = match Str.(split (regexp ":") l) with @@ -249,6 +256,7 @@ let parse_coqdep_line l = the platform. Anyways, I hope we can link to coqdep instead of having to parse its output soon, that should solve this kind of issues *) + let deps = List.map fix_cmo_cma deps in Some (String.split_on_char '/' dir, VO { target; deps; }) (* Otherwise a vio file, we ignore *) | _ -> None |