physlib/lakefile.lean at master · leanprover-community/physlib · 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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
import Lake
open System Lake DSL

package «PhysLib»

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

require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "v4.28.0"

@[default_target]
lean_lib PhysLean where
  moreLeanArgs := #[
    "-Dwarn.sorry=false"
  ]

@[default_target]
lean_lib QuantumInfo where
  moreLeanArgs := #[
    "-Dwarn.sorry=false"
  ]

-- These were their own lean_lib in Lean-QuantumInfo, we should move them to appropriate directories.
-- lean_lib ClassicalInfo
-- lean_lib StatMech

lean_exe check_file_imports where
  srcDir := "scripts"

lean_exe style_lint where
  srcDir := "scripts/MetaPrograms"

lean_exe type_former_lint where
  srcDir := "scripts"

lean_exe lint_all where
  supportInterpreter := true
  srcDir := "scripts"

lean_exe check_dup_tags where
  supportInterpreter := true
  srcDir := "scripts/MetaPrograms"

lean_exe sorry_lint where
  supportInterpreter := true
  srcDir := "scripts/MetaPrograms"

lean_exe runPhysLeanLinters where
  supportInterpreter := true
  srcDir := "scripts/MetaPrograms"

-- Other linting scripts

lean_exe free_simps where
  srcDir := "scripts/MetaPrograms"

lean_exe spelling where
  srcDir := "scripts/MetaPrograms"

lean_exe check_rfl where
  srcDir := "scripts/MetaPrograms"

lean_exe redundant_imports where
  supportInterpreter := true
  srcDir := "scripts/MetaPrograms"

lean_exe module_doc_lint where
  srcDir := "scripts/MetaPrograms"

-- Stats

lean_exe stats where
  supportInterpreter := true
  srcDir := "scripts"

lean_exe local_stats where
  supportInterpreter := true
  srcDir := "scripts/MetaPrograms"

-- Scripts for the website

lean_exe make_tag where
  supportInterpreter := true
  srcDir := "scripts/MetaPrograms"

lean_exe TODO_to_yml where
  supportInterpreter := true
  srcDir := "scripts/MetaPrograms"

lean_exe informal where
  supportInterpreter := true
  srcDir := "scripts/MetaPrograms"

-- Old

lean_exe find_TODOs where
  srcDir := "scripts"

lean_exe notes where
  supportInterpreter := true
  srcDir := "scripts/MetaPrograms"

lean_exe mathlib_textLint_on_hepLean where
  srcDir := "scripts"

lean_exe no_docs where
  srcDir := "scripts/MetaPrograms"

-- Optional scripts

-- Optional inclusion of llm. Needed for `openAI_doc_check`
-- require llm from git "https://github.com/leanprover-community/llm" @ "main"

-- Optional inclusion of tryAtEachStep
-- require tryAtEachStep from git "https://github.com/dwrensha/tryAtEachStep" @ "main"

-- Optional inclusion of LeanCopilot
-- require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.4.1"

-- lean_exe commands defined specifically for PhysLean.

-- Optional inclusion of openAI_doc_check. Needs `llm` above.
-- lean_exe openAI_doc_check where
--   srcDir := "scripts"