Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 3 additions & 6 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -55,12 +55,9 @@ jobs:
- name: Export Lean import graph
run: |
set -euo pipefail
mkdir -p .ci/lean/EvalTools
lean -R . -o .ci/lean/EvalTools/Markers.olean EvalTools/Markers.lean
LEAN_PATH="$PWD/.ci/lean" lean -R . \
-o .ci/lean/EvalTools/ModuleCoverage.olean EvalTools/ModuleCoverage.lean
LEAN_PATH="$PWD/.ci/lean" lean --run EvalTools/CIImportGraph.lean \
> .ci/import-graph.json
mkdir -p .ci
lake build EvalTools.CIImportGraph
lake env lean --run EvalTools/CIImportGraph.lean > .ci/import-graph.json

- name: Select affected catalog problems
id: changes
Expand Down
2 changes: 2 additions & 0 deletions EvalTools/CheckComparatorInstallation.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@ import EvalTools.Subprocess

namespace EvalTools

open LeanEvalGenerator.Core

set_option autoImplicit false

structure Semver where
Expand Down
2 changes: 2 additions & 0 deletions EvalTools/CheckEvalWorkflow.lean
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ open Lean

namespace EvalTools

open LeanEvalGenerator.Core

set_option autoImplicit false

private def TWO_PLUS_TWO_ID : String := "two_plus_two"
Expand Down
2 changes: 2 additions & 0 deletions EvalTools/CheckProblemBuild.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ import EvalTools.Manifest

namespace EvalTools

open LeanEvalGenerator.Core

set_option autoImplicit false

private def hasSubstr (haystack pattern : String) : Bool :=
Expand Down
Loading