fsm/lakefile.toml at trunk · escapace/fsm · 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
name = "Fsm"
version = "0.0.0"
defaultTargets = ["Fsm"]

[leanOptions]
relaxedAutoImplicit = false
maxSynthPendingDepth = 3

pp.unicode.fun = true

weak.linter.mathlibStandardSet = true

weak.linter.style.longLine = false

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

[[lean_lib]]
name = "Fsm"
srcDir = "lean"
roots = [
  "Defs",
  "Dispatch",
  "Determinism",
  "Soundness",
  "Reachability",
  "Validity",
  "Expansion",
  "Compose",
  "ComposeSoundness",
  "ComposeAssociativity",
  "Replay",
  "DraftDefs",
  "Draft",
  "DraftCommit",
  "DraftNested",
  "ProtocolDefs",
  "ProtocolDispatch",
  "ProtocolReplay",
  "ProtocolDraft",
  "ProtocolSoundness",
  "ProtocolReceiveDefs",
  "ProtocolReceiveDispatch",
  "ProtocolReceiveReplay",
  "ProtocolReceiveDraft",
  "ProtocolReceiveSoundness",
  "ProjectionDefs",
  "ProjectionNormalize",
  "ProjectionProject",
  "ProjectionPaths",
  "ProjectionInvariants",
  "ProjectionSoundness",
]

[[lean_lib]]
name = "Reconcile"
srcDir = "lean"
roots = [
  "Reconcile.Defs",
  "Reconcile.WF",
  "Reconcile.SnapshotSpec",
  "Reconcile.SnapshotSoundness",
  "Reconcile.ReconcileSpec",
  "Reconcile.ReconcileSoundness",
  "Reconcile.Algorithm",
  "Reconcile.Test",
]