diff options
| author | Gaëtan Gilbert | 2019-04-02 14:42:31 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-04-02 15:24:09 +0200 |
| commit | b9f3f8eda83ccfee7f7196f8f4d7584fb1cd9940 (patch) | |
| tree | f653e8410b2c7fd0b48d16769ca7e8204e70202a | |
| parent | 2f1111e4349c41e2d750795475241b919edc1fb6 (diff) | |
coqchk: use unsafe marshal for dependencies of -norec libraries
on test-suite/arithmetic/mod: 2.6s to 0.45s
| -rw-r--r-- | checker/check.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/checker/check.ml b/checker/check.ml index 76f85c86c9..a2c8a0f25d 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -328,6 +328,10 @@ let intern_from_file ~intern_mode (dir, f) = Flags.if_verbose chk_pp (str"[intern "++str f++str" ..."); let (sd,md,table,opaque_csts,digest) = try + let marshal_in_segment f ch = if intern_mode <> Dep + then marshal_in_segment f ch + else System.marshal_in_segment f ch + in let ch = System.with_magic_number_check raw_intern_library f in let (sd:summary_disk), _, digest = marshal_in_segment f ch in let (md:library_disk), _, digest = marshal_in_segment f ch in |