FloatSpec/lakefile.lean at main · Beneficial-AI-Foundation/FloatSpec · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
import Lake
open Lake DSL

/-- Main FloatSpec package -/
package FloatSpec where
  -- Lean options (typechecked!)
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩,
    ⟨`autoImplicit, true⟩,
    ⟨`relaxedAutoImplicit, false⟩,
    ⟨`linter.missingDocs, true⟩,
    ⟨`linter.unnecessarySimpa, false⟩,
    ⟨`linter.unusedSimpArgs, false⟩,
    -- Allow work-in-progress files that use `sorry` to compile
    ⟨`warningAsError, false⟩,
    -- Prefer grind over omega (weak. prefix allows setting before linter is loaded)
    ⟨`weak.linter.preferGrind, true⟩,
    -- Prefer simp over simp only for maintainability
    ⟨`weak.linter.preferSimp, true⟩,
    -- Avoid returning Id in definitions; keep Id only in mvcgen specs
    ⟨`weak.linter.noIdReturn, true⟩,
    -- Warn on non-True preconditions / trivial postconditions in Hoare triples
    ⟨`weak.linter.hoareStyle, true⟩
  ]
  -- Cloud release configuration for pre-built artifacts
  releaseRepo := "https://github.com/Beneficial-AI-Foundation/FloatSpec"
  buildArchive := "FloatSpec-{OS}-{ARCH}.tar.gz"
  preferReleaseBuild := false

/-! Dependencies -/

require cslib from git "https://github.com/leanprover/cslib" @ "v4.29.0"

require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.29.0"

/-- Linters for FloatSpec (prefer grind over omega, etc).
    Stdlib only, provides linter.preferGrind option.
-/
lean_lib FloatSpecLinter where
  globs := #[.andSubmodules `FloatSpec.Linter]

/-- Stub for doc-role registration (Verso/VersoCoq removed in this fork). -/
lean_lib FloatSpecRoles where
  globs := #[.one `FloatSpecRoles]

/-- Main library -/
@[default_target]
lean_lib FloatSpecLib where
  globs := #[.andSubmodules `FloatSpec.src, .one `FloatSpec, .one `FloatSpec.VersoExt]
  needs := #[FloatSpecLinter, FloatSpecRoles]

/-- Lightweight property tests (Plausible) and smoke checks. -/
lean_lib FloatSpecTests where
  globs := #[.andSubmodules `FloatSpec.Test]
  needs := #[FloatSpecLib]

/-- Executables -/
lean_exe floatspec where
  root := `Main

-- lean_exe floatspecmanual where
--   root := `FloatSpec.ManualMain