fix test framework and CI

leanprover · Nov 16, 2023 · ffa7217 · ffa7217
1 parent 19207d2
commit ffa7217
Show file tree

Hide file tree

Showing 10 changed files with 18 additions and 18 deletions.
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -1,5 +1,6 @@
 on:
   push:
+  pull_request:
 
 name: continuous integration
 

diff --git a/Lean4Checker.lean b/Lean4Checker.lean
@@ -1,4 +0,0 @@
-import Lean4Checker.Tests.AddFalse
-import Lean4Checker.Tests.AddFalseConstructor
-import Lean4Checker.Tests.ReduceBool
-import Lean4Checker.Tests.UseFalseConstructor

diff --git a/Lean4CheckerTests.lean b/Lean4CheckerTests.lean
diff --git a/Lean4Checker/Tests/AddFalse.lean → Lean4CheckerTests/AddFalse.lean b/Lean4Checker/Tests/AddFalse.lean → Lean4CheckerTests/AddFalse.lean
@@ -1,4 +1,4 @@
-import Lean4Checker.Tests.OpenPrivate
+import Lean4CheckerTests.OpenPrivate
 
 open private mk from Lean.Environment
 

diff --git a/Lean4Checker/Tests/AddFalseConstructor.lean → Lean4CheckerTests/AddFalseConstructor.lean b/Lean4Checker/Tests/AddFalseConstructor.lean → Lean4CheckerTests/AddFalseConstructor.lean
@@ -1,4 +1,4 @@
-import Lean4Checker.Tests.OpenPrivate
+import Lean4CheckerTests.OpenPrivate
 
 open private mk from Lean.Environment
 

diff --git a/Lean4Checker/Tests/OpenPrivate.lean → Lean4CheckerTests/OpenPrivate.lean b/Lean4Checker/Tests/OpenPrivate.lean → Lean4CheckerTests/OpenPrivate.lean
diff --git a/Lean4Checker/Tests/ReduceBool.lean → Lean4CheckerTests/ReduceBool.lean b/Lean4Checker/Tests/ReduceBool.lean → Lean4CheckerTests/ReduceBool.lean
diff --git a/Lean4Checker/Tests/UseFalseConstructor.lean → Lean4CheckerTests/UseFalseConstructor.lean b/Lean4Checker/Tests/UseFalseConstructor.lean → Lean4CheckerTests/UseFalseConstructor.lean
@@ -1,4 +1,4 @@
-import Lean4Checker.Tests.AddFalseConstructor
+import Lean4CheckerTests.AddFalseConstructor
 
 theorem useEvilConstructor : False :=
   False.intro
diff --git a/lakefile.lean b/lakefile.lean
@@ -3,10 +3,15 @@ open Lake DSL
 
 package «lean4checker» where
 
-@[default_target]
+ @[default_target]
 lean_lib «Lean4Checker» where
+  globs := #[.andSubmodules `Lean4Checker]
 
 @[default_target]
 lean_exe «lean4checker» where
   root := `Main
   supportInterpreter := true
+
+@[default_target]
+lean_lib «Lean4CheckerTests» where
+  globs := #[.andSubmodules `Lean4CheckerTests]
diff --git a/test.sh b/test.sh
@@ -1,8 +1,6 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-# Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
-# we just keep rebuilding until it works!
-until lake build > /dev/null 2>&1; do :; done
+lake build
 
 check_command() {
     local cmd="$1"
@@ -25,19 +23,19 @@ check_command() {
     fi
 }
 
-check_command "lake exe lean4checker Lean4Checker.Tests.AddFalse" "uncaught exception: (kernel) declaration type mismatch, 'false' has type
+check_command "lake exe lean4checker Lean4CheckerTests.AddFalse" "uncaught exception: (kernel) declaration type mismatch, 'false' has type
   Prop
 but it is expected to have type
   False"
 
-check_command "lake exe lean4checker Lean4Checker.Tests.AddFalseConstructor" "uncaught exception: No such constructor False.intro"
+check_command "lake exe lean4checker Lean4CheckerTests.AddFalseConstructor" "uncaught exception: No such constructor False.intro"
 
-check_command "lake exe lean4checker --fresh Lean4Checker.Tests.UseFalseConstructor" "uncaught exception: (kernel) unknown constant 'False.intro'"
+check_command "lake exe lean4checker --fresh Lean4CheckerTests.UseFalseConstructor" "uncaught exception: (kernel) unknown constant 'False.intro'"
 
+# The 'ReduceBool' test writes to a temporary file.
+# We clean up before and afterwards for consistency, although neither should be required.
 rm -f .lean4checker.tmp
-
-check_command "lake exe lean4checker Lean4Checker.Tests.ReduceBool" "uncaught exception: (kernel) unknown declaration 'foo'"
-
+check_command "lake exe lean4checker Lean4CheckerTests.ReduceBool" "uncaught exception: (kernel) unknown declaration 'foo'"
 rm -f .lean4checker.tmp
 
 echo "All commands produced the expected errors."