infra/Infra.lean at main · typednotes/infra · 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
-- This module serves as the root of the `Infra` library.
-- Import modules here that should be built as part of the library.

-- Core, bottom-up: the two axes, then specs, then fleets, then the engine.
import Infra.Core.Finite
import Infra.Core.Refine
import Infra.Core.Kind
import Infra.Core.Slot
import Infra.Core.Expr
import Infra.Core.Spec
import Infra.Core.Coe
import Infra.Core.InstanceType
import Infra.Core.Compose
import Infra.Specs.Kubernetes
import Infra.Specs.Basic
import Infra.Specs.Build
import Infra.Core.SqlDeps
import Infra.Core.Fleet
import Infra.Core.Ergonomics
import Infra.Core.Region
import Infra.Core.Bundle
import Infra.Core.Declare
import Infra.Core.Action
import Infra.Core.Backend
import Infra.Core.Diverge
import Infra.Core.Settle
import Infra.Core.Credentials
import Infra.Core.JsonExact
import Infra.Core.Image
import Infra.Core.Images
import Infra.Core.Ownership
import Infra.Core.Engine

-- Authentication is orthogonal to the resource theory above.
import Infra.Core.Auth
import Infra.Abstractions.Auth

-- One backend per cloud.
import Infra.Providers.JsonRead
import Infra.Providers.Http
import Infra.Providers.Images
import Infra.Providers.Zip
import Infra.Providers.Aws.Sign
import Infra.Providers.Aws.Protocols
import Infra.Providers.Scaleway.Rest
import Infra.Providers.Kinds.ObjectStore
import Infra.Providers.Kinds.Queues
import Infra.Providers.Kinds.ImageRegistry
import Infra.Providers.Kinds.Secrets
import Infra.Providers.Kinds.Compute
import Infra.Providers.Kinds.Iam
import Infra.Providers.Kinds.Postgres
import Infra.Providers.Kinds.Migrations
import Infra.Providers.Kube.Client
import Infra.Providers.Kinds.Kubernetes
import Infra.Providers.Kinds.Ec2
import Infra.Providers.Kinds.Identity
import Infra.Providers.Gcp
import Infra.Providers.Live
import Infra.Providers

-- Interoperability with the tool this replaces, both directions.
import Infra.Interop.Terraform
import Infra.Interop.Yaml
import Infra.Interop.KubernetesYaml

-- The command-line front end, so a declaration repo's `Main` is a call rather
-- than a copy of the dispatch.
import Infra.Cli
import Infra.Cli.New

import Infra.Demo