use lake test for testing

.github/workflows/main.yml

@@ -36,7 +36,7 @@ jobs:
         with:
           build-args: "--log-level=error"
       - name: Run Tests
-        run: make test
+        run: lake test
       - name: Run Examples
         run: make examples
       - name: Setup Pages

SciLean/Modules/DDG/SurfaceMesh.lean

@@ -294,18 +294,18 @@ partial def MeshBuilderM.build_
   modify (fun s => { s with positions := positions }); -- store positions in the SurfaceMesh
 
   -- pre-allocate all vertices for random access via faces.
-  for _ in List.range positions.size do {
+  for _ in Array.range positions.size do {
       let _ ← newVertex;
   }
   assert! (indices.size % 3 == 0);
-  for i in List.range (indices.size / 3) do {
+  for i in Array.range (indices.size / 3) do {
     let I := i * 3;
     let f ← newFace;
     -- create a halfedge for each edge of the newly created face
-    for _ in List.range 3 do {
+    for _ in Array.range 3 do {
       let _ ← newHalfedge; -- make the new half edges
     }
-    for J in List.range 3 do {
+    for J in Array.range 3 do {
       -- current halfedge goes from vertex i to vertex j
       let K : Nat := (J + 1) % 3;
       let i := I + J;
@@ -362,7 +362,7 @@ partial def MeshBuilderM.build_
   -- also create and insert corners.
   -- Note that every vertex corresponds to the halfedge from that vertex to
   --   the next one in the triangle.
-  for i in List.range indices.size do {
+  for i in Array.range indices.size do {
     let h ← getHalfedge i;
     -- If a halfedge has no twin halfedge, create a new face and
     -- link it the corresponding boundary cycle
@@ -428,7 +428,7 @@ def randVertices [RandomGen γ]
  (gen : γ) (nvertices : Nat) (scale : Float := 10) : (Array (SciLean.Vec3)) × γ := Id.run do
   let mut out : Array (SciLean.Vec3) := #[]
   let mut gen := gen
-  for _ in List.range nvertices do
+  for _ in Array.range nvertices do
     let (vertex, gen') := randVertex01 gen; gen := gen'
     let vertex : (SciLean.Vec3) := SciLean.ArrayType.mapMono (fun coord => (coord - 0.5) * scale) vertex
     out := out.push vertex
@@ -446,7 +446,7 @@ def randTriFace [RandomGen γ] (gen : γ) (nvertices : Nat) : (Array Nat) × γ
 def randTriFaces [RandomGen γ] (gen : γ) (nvertices : Nat) (nfaces : Nat) : (Array Nat) × γ := Id.run do
   let mut out : Array Nat := #[]
   let mut gen := gen
-  for _ in List.range nfaces do
+  for _ in Array.range nfaces do
     let (face, gen') := randTriFace gen nvertices; gen := gen'
     out := out.append face
   return (out, gen)
@@ -486,7 +486,7 @@ def SurfaceMesh.fromOFFString (lines : Array String) : MeshBuilderM Unit := do
   let .some n_faces := n_faces.toNat?
     | throw <| MeshBuilderError.parseError s! "unable to parse num faces {n_faces}"
 
-  for _ in List.range n_vertices do
+  for _ in Array.range n_vertices do
     let coords_raw := lines[i]!.trim.splitOn " "
     let mut v : Array Float := #[]
     for coord in coords_raw do
@@ -496,13 +496,15 @@ def SurfaceMesh.fromOFFString (lines : Array String) : MeshBuilderM Unit := do
     vertices := vertices.push (← V3.ofArray v)
     i := i + 1
 
-  for _ in List.range n_faces do
+  for _ in [0:n_faces] do
     let face_indexes_raw := lines[i]!.trim.splitOn " "
     let mut f : Array Nat := #[]
     for ix in face_indexes_raw.drop 1 do
       let .some ix := ix.toNat?
-        | throw <| MeshBuilderError.parseError s!"unable to parse face index {ix} on line {i+1}"
-        f := f.push ix
+        -- ".. on line {i+1}" -- for some reason adding {i+1} cause stack overflow
+        -- this looks like a compiler bug
+        | throw <| MeshBuilderError.parseError s!"unable to parse face index {ix} on line ..."
+      f := f.push ix
     faces := faces.append f
     i := i + 1
   MeshBuilderM.build_ vertices faces

Test/calculus/monad_test.lean

@@ -0,0 +1,82 @@
+import SciLean
+
+
+-- there are some linker issues :(
+#exit
+
+open SciLean
+
+
+variable (R : Type) [RealScalar R]
+
+set_default_scalar R
+
+
+/--
+info: fun x =>
+  let zdz := x * x;
+  let ydy := zdz ^ 3;
+  let ydy := ydy + ydy;
+  fun dx =>
+  let zdz_1 := x * dx + dx * x;
+  let ydy_1 := 3 * zdz_1 * zdz ^ 2;
+  let ydy_2 := ydy_1 + ydy_1;
+  (ydy, ydy_2) : R → R → R × R
+-/
+#guard_msgs in
+#check (∂> (x : R), Id'.run do
+         let mut x := x
+         x := x*x
+         x := x^3
+         x := x+x
+         return x) rewrite_by autodiff
+
+
+variable (a b : R)
+
+
+#check (fwdFDeriv R fun x : R => Id'.run do
+         let mut x := x
+         if h : a < b then
+           x := x^3
+         if 0 < b then
+           x := x^4
+         if 0 < a then
+           x := x^5
+         return x) rewrite_by
+  fun_trans (config:={zeta:=false}) only [simp_core]
+  let_normalize (config:={removeLambdaLet:=false,removeNoFVarLet:=true})
+  fun_trans (config:={zeta:=false}) only [simp_core]
+  lsimp (config:={singlePass:=true})
+  lsimp (config:={singlePass:=true})
+
+
+#check (fwdFDeriv R (fun x : R =>
+       let f := fun y : R => y
+       f x)) rewrite_by fun_trans (config:={zeta:=false}) -- nothing happens :(
+
+
+set_option linter.unusedTactic false
+example : Differentiable R ((fun x : R =>
+       let f := fun y : R => y + x
+       f x)) := by (try fun_prop); sorry_proof -- fun_prop does not work :(
+
+
+-- #check (fwdFDeriv R fun x : R => Id'.run do
+--          let mut x := x
+--          x := x^2
+--          if a < b then
+--            x := x^3
+--          if 0 < b then
+--            x := x^4
+--          if 0 < a then
+--            x := x^5
+--          return x) rewrite_by autodiff (disch:=simp only [simp_core])
+
+-- #guard_msgs in
+-- #check (<∂ (x : R), Id'.run do
+--          let mut x := x
+--          x := x*x
+--          x := x^3
+--          x := x+x
+--          return x) rewrite_by autodiff

Test/calculus/revFDerivProj_test.lean

@@ -0,0 +1,61 @@
+import SciLean
+
+open SciLean
+
+variable {R : Type} [RealScalar R] [PlainDataType R]
+  {n : Nat}
+
+
+set_default_scalar R
+
+
+/--
+info: fun x =>
+  IndexType.foldl
+    (fun dx i =>
+      let dx := ArrayType.modify dx i fun xi => xi + 1;
+      dx)
+    0 : R^[n] → R^[n]
+-/
+#guard_msgs in
+#check (∇ (x : R^[n]), ∑ i, x[i]) rewrite_by autodiff
+
+
+/--
+info: fun x =>
+  IndexType.foldl
+    (fun dx i =>
+      let ydf := x[i];
+      let y' := 2 * ydf;
+      let dx := ArrayType.modify dx i fun xi => xi + y';
+      dx)
+    0 : R^[n] → R^[n]
+-/
+#guard_msgs in
+#check (∇ (x : R^[n]), ∑ i, x[i]^2) rewrite_by autodiff
+
+
+variable (A : R^[n,n])
+
+
+/--
+info: fun x =>
+  IndexType.foldl
+    (fun dx i =>
+      let zdg := x[i];
+      let dx :=
+        IndexType.foldl
+          (fun dx i_1 =>
+            let ydf := A[i, i_1];
+            let ydf_1 := ydf * zdg;
+            let zdg := x[i_1];
+            let dy₂ := ydf * zdg;
+            let dx := ArrayType.modify dx i_1 fun xi => xi + ydf_1;
+            let dx := ArrayType.modify dx i fun xi => xi + dy₂;
+            dx)
+          dx;
+      dx)
+    0 : R^[n] → R^[n]
+-/
+#guard_msgs in
+#check (∇ (x : R^[n]), ∑ i j, A[i,j]*x[i]*x[j]) rewrite_by autodiff