Disable backend tracing as it breaks Linux builds

marcusrossel · Apr 15, 2024 · 2c67b4f · 2c67b4f
1 parent b5df0cd
commit 2c67b4f
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 6 deletions.
diff --git a/C/ffi.c b/C/ffi.c
@@ -131,10 +131,12 @@ lean_obj_res run_egg_request(lean_obj_arg req) {
     return lean_mk_string(result);
 }
 
+/*
 lean_object* dbg_trace_thunk(lean_object* t) { return lean_box(0); }
 void c_dbg_trace(char const* str) {
     lean_object* thunk_obj = lean_alloc_closure(&dbg_trace_thunk, 1, 0);
     lean_object* lstr = lean_mk_string(str);
     lean_dbg_trace(lstr, thunk_obj);
     return;
-}
+}
+*/
diff --git a/Lean/Egg/Core/Config.lean b/Lean/Egg/Core/Config.lean
@@ -31,6 +31,7 @@ inductive Debug.ExitPoint
 structure Debug where
   exitPoint           := Debug.ExitPoint.none
   vizPath             := (none : Option String)
+  -- TODO: Debug tracing is currently disabled in Rust as it breaks builds on Linux.
   traceSubstitutions  := false
   traceBVarCorrection := false
   deriving BEq

diff --git a/Lean/Egg/Tests/Freshman.lean b/Lean/Egg/Tests/Freshman.lean
@@ -32,7 +32,8 @@ class CharTwoRing (α) extends Ring α where
 
 open Ring CharTwoRing Egg.Guides Egg.Config.Modifier in
 macro "char_two_ring" mod:egg_cfg_mod base:(egg_base)? guides:(egg_guides)? : tactic => `(tactic|
-  egg $mod [comm_add, comm_mul, add_assoc, mul_assoc, sub_canon, neg_add, div_canon, zero_add, zero_mul, one_mul, distrib, pow_zero, pow_one, pow_two, pow_three, char_two] $[$base]? $[$guides]?
+  egg $mod [comm_add, comm_mul, add_assoc, mul_assoc, sub_canon, neg_add, div_canon, zero_add,
+  zero_mul, one_mul, distrib, pow_zero, pow_one, pow_two, pow_three, char_two] $[$base]? $[$guides]?
 )
 
 variable [CharTwoRing α]
@@ -48,7 +49,7 @@ theorem freshmans_dream' (x y : α) : (x + y) ^ 2 = (x ^ 2) + (y ^ 2) := by
   char_two_ring
 
 theorem freshmans_dream₃ (x y : α) : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
-  calc (x + y)^ 3
+  calc (x + y) ^ 3
    _ = (x + y) * (x + y) * (x + y)                     := by char_two_ring
    _ = (x + y) * (x * (x + y) + y * (x + y))           := by char_two_ring
    _ = (x + y) * (x ^ 2 + x * y + y * x + y ^ 2)       := by char_two_ring

diff --git a/Rust/src/trace.rs b/Rust/src/trace.rs
@@ -1,11 +1,13 @@
-use std::ffi::c_char;
-use std::ffi::CString;
+// use std::ffi::c_char;
+// use std::ffi::CString;
 use std::collections::HashSet;
 use std::hash::Hash;
 
+/*
 extern "C" {
     fn c_dbg_trace(str: *const c_char);
 }
+*/
 
 static mut ENABLED_TRACE_GROUPS: Option<HashSet<TraceGroup>> = None;
 
@@ -22,14 +24,16 @@ pub fn init_enabled_trace_groups(trace_substitutions: bool, trace_bvar_correctio
     unsafe { ENABLED_TRACE_GROUPS = Some(enabled) }
 }
 
-pub fn dbg_trace<T: ToString>(obj: T, group: TraceGroup) {
+pub fn dbg_trace<T: ToString>(_obj: T, group: TraceGroup) {
     unsafe { 
         if let Some(enabled) = &ENABLED_TRACE_GROUPS { 
             if !enabled.contains(&group) { return } 
         } 
     }
 
+    /* 
     let str = obj.to_string();
     let c_str = CString::new(str).expect("conversion of explanation to C-string failed");
     unsafe { c_dbg_trace(c_str.into_raw()) }
+    */
 }