lakefile.toml

# Copyright 2025 The Formal Conjectures Authors.
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#     https://www.apache.org/licenses/LICENSE-2.0
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.

name = "formal_conjectures"
keywords = ["math"]
defaultTargets = ["FormalConjectures"]
testDriver = "FormalConjecturesTest"

[leanOptions]
# Pretty-prints `fun a ↦ b`
pp.unicode.fun = true
# Don't assume a typo is a new variable
autoImplicit = false
relaxedAutoImplicit = false

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.27.0"

# We make this a separate library so that we can apply different lean options.
[[lean_lib]]
name = "FormalConjecturesForMathlib"

[[lean_lib]]
name = "FormalConjecturesTest"
# Switch off warnings generated by `sorry`
leanOptions = { warn.sorry = false }

[[lean_lib]]
name = "FormalConjectures"
globs = ["FormalConjectures.+"]
# Switch off warnings generated by `sorry`
leanOptions = { warn.sorry = false }

[[lean_exe]]
name = "extract_names"
srcDir = "scripts"
root = "extract_names"
exeName = "extract_names"
supportInterpreter = true