Add a check in Driver.ml

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