lean-beam/lakefile.lean at main · leanprover/lean-beam · 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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
/-
Copyright (c) 2026 Lean FRO LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Emilio J. Gallego Arias
-/

import Lake

open Lake DSL
open System

package "beam" where
  enableArtifactCache := true
  restoreAllArtifacts := true

target beamControlDirObj (pkg) : FilePath := do
  let srcFile := pkg.dir / "Beam" / "Native" / "control_dir.c"
  let oFile := pkg.buildDir / "native" / "control_dir.o"
  let srcTarget ← inputTextFile srcFile
  buildFileAfterDep oFile srcTarget fun srcFile => do
    compileO oFile srcFile #["-I", (← getLeanIncludeDir).toString, "-fPIC"]

lean_lib Beam.LSP where
  globs := #[.andSubmodules `Beam.LSP]
  defaultFacets := #[`shared]

lean_lib Beam where
  defaultFacets := #[`shared]
  moreLinkObjs := #[beamControlDirObj]

lean_lib BeamTest where
  srcDir := "tests/lean"

lean_exe "beam-lsp-test" where
  srcDir := "tests/lean"
  root := `BeamTest.LSP.TestRunner

lean_exe "beam-lsp-scenario-test" where
  srcDir := "tests/lean"
  root := `BeamTest.LSP.ScenarioRunner

lean_exe "beam-lsp-scenario-api-test" where
  srcDir := "tests/lean"
  root := `BeamTest.LSP.Scenario.ApiTest

lean_exe "beam-lsp-scenario-stress-test" where
  srcDir := "tests/lean"
  root := `BeamTest.LSP.Scenario.StressTest

lean_exe "beam-lsp-handle-api-test" where
  srcDir := "tests/lean"
  root := `BeamTest.LSP.Handle.ApiTest

lean_exe "beam-lsp-handle-restart-test" where
  srcDir := "tests/lean"
  root := `BeamTest.LSP.Handle.RestartTest

lean_exe "beam-lsp-handle-lifecycle-test" where
  srcDir := "tests/lean"
  root := `BeamTest.LSP.Handle.LifecycleTest

lean_exe "beam-lsp-mcts-proof-search-test" where
  srcDir := "tests/lean"
  root := `BeamTest.LSP.Scenario.MctsProofSearchTest

lean_exe "beam-lsp-parallel-grind-batch-test" where
  srcDir := "tests/lean"
  root := `BeamTest.LSP.Scenario.ParallelGrindBatchTest

lean_exe "beam-lsp-nested-handle-failure-test" where
  srcDir := "tests/lean"
  root := `BeamTest.LSP.Handle.NestedHandleFailureTest

lean_exe "beam-lsp-request-surface-test" where
  srcDir := "tests/lean"
  root := `BeamTest.LSP.RequestSurfaceTest

lean_exe "beam-lsp-search-workload-report" where
  srcDir := "tests/lean"
  root := `BeamTest.LSP.Scenario.SearchWorkloadReport

lean_exe "beam-daemon" where
  root := `Beam.Broker.ServerMain
  supportInterpreter := true

lean_exe "beam-client" where
  root := `Beam.BrokerClient

lean_exe "lean-beam-mcp" where
  root := `Beam.Mcp.ServerMain
  supportInterpreter := true

@[default_target]
lean_exe "beam-cli" where
  root := `Beam.Cli

lean_exe "beam-daemon-smoke-test" where
  srcDir := "tests/lean"
  root := `BeamTest.Broker.SmokeTestMain

lean_exe "beam-sync-concurrency-test" where
  srcDir := "tests/lean"
  root := `BeamTest.Broker.SyncConcurrencyProbe

lean_exe "beam-daemon-save-stream-test" where
  srcDir := "tests/lean"
  root := `BeamTest.Broker.SaveStreamTestMain

lean_exe "beam-daemon-request-stream-test" where
  srcDir := "tests/lean"
  root := `BeamTest.Broker.RequestStreamContractTestMain

lean_exe "beam-sync-result-test" where
  srcDir := "tests/lean"
  root := `BeamTest.Broker.SyncResultTest

lean_exe "beam-daemon-startup-handshake-test" where
  srcDir := "tests/lean"
  root := `BeamTest.Broker.StartupHandshakeTestMain

lean_exe "beam-broker-protocol-test" where
  srcDir := "tests/lean"
  root := `BeamTest.Broker.ProtocolTest

lean_exe "beam-broker-pending-test" where
  srcDir := "tests/lean"
  root := `BeamTest.Broker.PendingTest

lean_exe "beam-broker-document-state-test" where
  srcDir := "tests/lean"
  root := `BeamTest.Broker.DocumentStateTest

lean_exe "beam-broker-open-docs-test" where
  srcDir := "tests/lean"
  root := `BeamTest.Broker.OpenDocsTest

lean_exe "beam-cli-daemon-test" where
  srcDir := "tests/lean"
  root := `BeamTest.Broker.CliDaemonTest

lean_exe "beam-feedback-test" where
  srcDir := "tests/lean"
  root := `BeamTest.Broker.FeedbackTest

lean_exe "beam-mcp-projection-test" where
  srcDir := "tests/lean"
  root := `BeamTest.Broker.McpProjectionTest

lean_exe "beam-mcp-protocol-test" where
  srcDir := "tests/lean"
  root := `BeamTest.Broker.McpProtocolTest

lean_exe "beam-daemon-rocq-smoke-test" where
  srcDir := "tests/lean"
  root := `BeamTest.Broker.RocqSmokeTest