search

argumentcomputer / yatima

A zero-knowledge Lean4 compiler and kernel
MIT License
122 stars 9 forks source link

in Windows, `lake run import_all` does not work #281

Closed Seasawher closed 10 months ago

Seasawher commented 1 year ago

The reason is a difference in the path delimiter.

I suggest a following change: 👍 

def getImportsString : ScriptM String := do
  let paths ← getAllFiles
  let imports := paths.map fun p =>
    "import " ++ ((p.splitOn ".").head!.replace "/" ".").replace "\\" "."
  return s!"{"\n".intercalate imports}\n"