From bd7ef0f9d45d10b4439e125d006b2dd4319fd1c9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 7 Mar 2023 12:12:32 +0100
Subject: Add a check in Driver.ml

---
 compiler/Driver.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'compiler')

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
 
-- 
cgit v1.2.3