fix: macos ci, Lake.inputFile -> Lake.inputTextFile (#2)

* fix: macos ci, Lake.inputFile -> Lake.inputTextFile

* fix: typo

* fix: only run proc test when /proc is available

.github/workflows/ci.yml

@@ -49,8 +49,8 @@ jobs:
 
       - name: Build everything
         run: |
-          LD_LIBRARY_PATH=/usr/local/lib lake build
+          DYLD_LIBRARY_PATH=/usr/local/lib LD_LIBRARY_PATH=/usr/local/lib lake build
 
       - name: Run the test
         run: |
-          LD_LIBRARY_PATH=/usr/local/lib lake exe test
+          DYLD_LIBRARY_PATH=/usr/local/lib LD_LIBRARY_PATH=/usr/local/lib lake exe test

Test.lean

@@ -42,13 +42,15 @@ namespace proc
 
   --/ Get name of process using /proc/self/status
   def test : IO Unit := do
-    let m := 
-      Manifest.new #[Wasm.file "wasm/extproc.wasm"]
-      |> Manifest.allowPath "/proc" "/proc"
-    let plugin <- Plugin.new m #[] True
-    let res: Json Status <- Plugin.call plugin "status" ""
-    assert! res.val.name == "test"
-    IO.println s!"Name: {res.val.name}"
+    let ex <- System.FilePath.pathExists "/proc"
+    if ex then 
+      let m := 
+        Manifest.new #[Wasm.file "wasm/extproc.wasm"]
+        |> Manifest.allowPath "/proc" "/proc"
+      let plugin <- Plugin.new m #[] True
+      let res: Json Status <- Plugin.call plugin "status" ""
+      assert! res.val.name == "test"
+      IO.println s!"Name: {res.val.name}"
 end proc
 
 structure VowelCount where

lakefile.lean

@@ -32,7 +32,7 @@ lean_exe test {
 
 target bindings.o pkg : FilePath := do
   let oFile := pkg.buildDir / "c" / "bindings.o"
-  let srcJob ← inputFile <| pkg.dir / "c" / "bindings.c"
+  let srcJob ← inputTextFile <| pkg.dir / "c" / "bindings.c"
   let weakArgs := #["-I", (← getLeanIncludeDir).toString, "-I", extismIncludePath ()]
   buildO oFile srcJob weakArgs #["-fPIC", "--std=c11"] "cc" getLeanTrace