diff options
author | Son Ho | 2023-03-07 12:12:32 +0100 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | bd7ef0f9d45d10b4439e125d006b2dd4319fd1c9 (patch) | |
tree | b4e22b4347c3a1c9b8b387a01a6985142933de23 /compiler | |
parent | 40a08afb20dd9bb36069407e3db37a03a8be0981 (diff) |
Add a check in Driver.ml
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/Driver.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/compiler/Driver.ml b/compiler/Driver.ml index e0504903..e7425122 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -199,6 +199,18 @@ let () = in if has_loops then log#lwarning (lazy "Support for loops is experimental"); + (* If we target Lean, we request the crates to be split into several files + whenever there are opaque functions *) + if + !backend = Lean + && List.exists (fun (d : A.fun_decl) -> d.body = None) m.functions + && not !split_files + then ( + log#error + "For Lean, we request the -split-file option whenever using opaque \ + functions"; + fail ()); + (* Apply the pre-passes *) let m = PrePasses.apply_passes m in |