calling canonical from executable

Stream: general

[Frederick Pu]

I'm trying to call canonical from an executable:

import Canonical
import Lean

open Lean Meta Elab

def runMetaFromEnv (fileName : String) (fileMap : FileMap) (env : Environment) (m : MetaM α) : IO α := do
  let ctx : Core.Context := { fileName, fileMap}
  let st  : Core.State   := { env}
  let temp ← ((m.run').run' ctx st).toIO'
  match temp with
  | .ok a => pure a
  | .error e => throw <| IO.userError (← e.toMessageData.toString)


def testCanonical : MetaM Unit := do
  let α := mkSort levelZero
  let mvar ← mkFreshExprMVar α
  IO.println s!"mvar before: {mvar}"
  let (ty, mvar', reconstruct) ← Canonical.preprocessCanonical mvar.mvarId! #[] {}
  let outs ← Canonical.runCanonical ty mvar' reconstruct 5 {}
  IO.println "ran canonical"

def main : IO Unit := do
  let setup := do
    let temp ← IO.FS.realPath ".lake/packages/Canonical/.lake/build/lib/libcanonical_lean.so"
    IO.println s!"Loading dynlib from {temp}"
    Lean.loadDynlib temp
    let temp1 ← IO.FS.realPath ".lake/packages/Canonical/.lake/build/lib/libCanonical.so"
    IO.println s!"Loading dynlib from {temp1}"
    Lean.loadDynlib temp1
  setup
  IO.println "starting"
  let fileName : System.FilePath := "./Training/Test/TestExtractData/ban.lean"
  let input ← IO.FS.readFile fileName
  let fileMap := FileMap.ofString input
  let inputCtx := Parser.mkInputContext input fileName.toString
  let (header, parserState, messages) ← Parser.parseHeader inputCtx
  let (env, messages) ← processHeader header {} messages inputCtx
  runMetaFromEnv fileName.toString fileMap env testCanonical

however, even after loaoding both dynlibs i still getting the following error:

(base) frederick-pu@frederick-pu-IdeaPad-5-2-in-1-16AHP9:~/Downloads/CanonicalDrafter/CanonicalDrafter$ lake env .lake/build/bin/mwe
Loading dynlib from /home/frederick-pu/Downloads/CanonicalDrafter/CanonicalDrafter/.lake/packages/Canonical/.lake/build/lib/libcanonical_lean.so
Loading dynlib from /home/frederick-pu/Downloads/CanonicalDrafter/CanonicalDrafter/.lake/packages/Canonical/.lake/build/lib/libCanonical.so
starting
mvar before: ?_uniq.1
PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none
backtrace:
.lake/build/bin/mwe(+0xa0a9e4e) [0x58aad7b13e4e]
.lake/build/bin/mwe(lean_panic_fn+0x1c) [0x58aad7b142ec]
.lake/build/bin/mwe(l_Destruct_destructCanonical___lam__1+0x2a8) [0x58aacff191c8]
.lake/build/bin/mwe(l_Destruct_destructCanonical___lam__1___boxed+0x20) [0x58aacff1aac0]
.lake/build/bin/mwe(lean_apply_5+0x58e) [0x58aad7b2666e]
.lake/build/bin/mwe(l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___redArg+0x1e2) [0x58aad2b37762]
.lake/build/bin/mwe(l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp+0x26) [0x58aad2b378c6]
.lake/build/bin/mwe(l_Lean_MVarId_withContext___at_____private_Lean_PremiseSelection_MePo_0__Lean_MVarId_getConstants_spec__9___redArg+0x25) [0x58aad003e0a5]
.lake/build/bin/mwe(l_Destruct_destructCanonical+0x2ce) [0x58aacff1a92e]
.lake/build/bin/mwe(l_Canonical_preprocess+0xa0) [0x58aacff27e80]
.lake/build/bin/mwe(l_Canonical_preprocessCanonical+0x5a7) [0x58aacff29d57]
.lake/build/bin/mwe(l_testCanonical+0x413) [0x58aacfdfffb3]
.lake/build/bin/mwe(lean_apply_5+0x6a) [0x58aad7b2614a]
.lake/build/bin/mwe(l_runMetaFromEnv___redArg+0x637) [0x58aacfdff3b7]
.lake/build/bin/mwe(+0x2398db3) [0x58aacfe02db3]
/lib/x86_64-linux-gnu/libc.so.6(+0x2a1ca) [0x79b15742a1ca]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x8b) [0x79b15742a28b]
.lake/build/bin/mwe(_start+0x2a) [0x58aacfdfecea]
PANIC at Lean.ConstantInfo.value! Lean.Declaration:489:31: declaration with value expected, but [anonymous] has none
backtrace:
.lake/build/bin/mwe(+0xa0a9e4e) [0x58aad7b13e4e]
.lake/build/bin/mwe(lean_panic_fn+0x1c) [0x58aad7b142ec]
.lake/build/bin/mwe(l_Destruct_destructCanonical___lam__1+0x2b5) [0x58aacff191d5]
.lake/build/bin/mwe(l_Destruct_destructCanonical___lam__1___boxed+0x20) [0x58aacff1aac0]
.lake/build/bin/mwe(lean_apply_5+0x58e) [0x58aad7b2666e]
.lake/build/bin/mwe(l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___redArg+0x1e2) [0x58aad2b37762]
.lake/build/bin/mwe(l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp+0x26) [0x58aad2b378c6]
.lake/build/bin/mwe(l_Lean_MVarId_withContext___at_____private_Lean_PremiseSelection_MePo_0__Lean_MVarId_getConstants_spec__9___redArg+0x25) [0x58aad003e0a5]
.lake/build/bin/mwe(l_Destruct_destructCanonical+0x2ce) [0x58aacff1a92e]
.lake/build/bin/mwe(l_Canonical_preprocess+0xa0) [0x58aacff27e80]
.lake/build/bin/mwe(l_Canonical_preprocessCanonical+0x5a7) [0x58aacff29d57]
.lake/build/bin/mwe(l_testCanonical+0x413) [0x58aacfdfffb3]
.lake/build/bin/mwe(lean_apply_5+0x6a) [0x58aad7b2614a]
.lake/build/bin/mwe(l_runMetaFromEnv___redArg+0x637) [0x58aacfdff3b7]
.lake/build/bin/mwe(+0x2398db3) [0x58aacfe02db3]
/lib/x86_64-linux-gnu/libc.so.6(+0x2a1ca) [0x79b15742a1ca]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x8b) [0x79b15742a28b]
.lake/build/bin/mwe(_start+0x2a) [0x58aacfdfecea]
PANIC at Canonical.apply Canonical.Util:118:11: apply: expected a lambda, got {e}
backtrace:
.lake/build/bin/mwe(+0xa0a9e4e) [0x58aad7b13e4e]
.lake/build/bin/mwe(lean_panic_fn+0x1c) [0x58aad7b142ec]
.lake/build/bin/mwe(l_Destruct_destructCanonical___lam__1+0x323) [0x58aacff19243]
.lake/build/bin/mwe(l_Destruct_destructCanonical___lam__1___boxed+0x20) [0x58aacff1aac0]
.lake/build/bin/mwe(lean_apply_5+0x58e) [0x58aad7b2666e]
.lake/build/bin/mwe(l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___redArg+0x1e2) [0x58aad2b37762]
.lake/build/bin/mwe(l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp+0x26) [0x58aad2b378c6]
.lake/build/bin/mwe(l_Lean_MVarId_withContext___at_____private_Lean_PremiseSelection_MePo_0__Lean_MVarId_getConstants_spec__9___redArg+0x25) [0x58aad003e0a5]
.lake/build/bin/mwe(l_Destruct_destructCanonical+0x2ce) [0x58aacff1a92e]
.lake/build/bin/mwe(l_Canonical_preprocess+0xa0) [0x58aacff27e80]
.lake/build/bin/mwe(l_Canonical_preprocessCanonical+0x5a7) [0x58aacff29d57]
.lake/build/bin/mwe(l_testCanonical+0x413) [0x58aacfdfffb3]
.lake/build/bin/mwe(lean_apply_5+0x6a) [0x58aad7b2614a]
.lake/build/bin/mwe(l_runMetaFromEnv___redArg+0x637) [0x58aacfdff3b7]
.lake/build/bin/mwe(+0x2398db3) [0x58aacfe02db3]
/lib/x86_64-linux-gnu/libc.so.6(+0x2a1ca) [0x79b15742a1ca]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x8b) [0x79b15742a28b]
.lake/build/bin/mwe(_start+0x2a) [0x58aacfdfecea]
uncaught exception: Unknown constant `_inhabitedExprDummy`

i was able to use the dynlib trick in past for lean repl but it's not working now for some reason
https://github.com/leanprover-community/repl/issues/115