Skip to content

Commit 97cde50

Browse files
author
Jonathan D.A. Jewell
committed
Auto-commit: Sync changes [2026-02-10]
1 parent 2908548 commit 97cde50

45 files changed

Lines changed: 1209 additions & 621 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.containerization/Containerfile‎

Lines changed: 127 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,127 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# SPDX-FileCopyrightText: 2024-2025 Jonathan D.A. Jewell <jonathan.jewell@open.ac.uk>
3+
#
4+
# ECHIDNA Minimal Containerfile - Multi-stage build for Podman
5+
# Uses chainguard base images for supply chain security.
6+
# Builds Rust binary, bundles Idris2, Z3, CVC5 for runtime verification.
7+
# For the full image with all provers, see Containerfile.full
8+
#
9+
# Build: podman build -f .containerization/Containerfile -t echidna:latest .
10+
# Seal: selur seal echidna:latest
11+
# Sign: cerro-torre sign echidna:latest
12+
13+
# =============================================================================
14+
# Stage 1: Rust Builder (wolfi has rust toolchain)
15+
# =============================================================================
16+
FROM cgr.dev/chainguard/wolfi-base:latest AS rust-builder
17+
18+
RUN apk add --no-cache \
19+
rust \
20+
cargo \
21+
build-base \
22+
pkgconf \
23+
openssl-dev
24+
25+
WORKDIR /build
26+
27+
COPY Cargo.toml Cargo.lock ./
28+
COPY src/rust ./src/rust
29+
COPY src/interfaces ./src/interfaces
30+
31+
# Build release binary
32+
RUN cargo build --release --bin echidna
33+
34+
# =============================================================================
35+
# Stage 2: Idris2 Builder
36+
# =============================================================================
37+
FROM cgr.dev/chainguard/wolfi-base:latest AS idris2-builder
38+
39+
RUN apk add --no-cache \
40+
curl \
41+
ca-certificates \
42+
tar \
43+
gzip \
44+
gmp-dev
45+
46+
WORKDIR /build
47+
48+
# Install Idris2 0.8.0 from official release
49+
RUN curl -fsSL "https://github.com/idris-lang/Idris2/releases/download/v0.8.0/Idris2-0.8.0-Linux-x86_64.tar.gz" \
50+
-o /tmp/idris2.tar.gz && \
51+
mkdir -p /opt/idris2 && \
52+
tar -xzf /tmp/idris2.tar.gz -C /opt/idris2 --strip-components=1 && \
53+
rm /tmp/idris2.tar.gz
54+
55+
# Copy and compile echidna-validator
56+
COPY src/idris /build/idris
57+
RUN export PATH="/opt/idris2/bin:$PATH" && \
58+
export IDRIS2_PREFIX="/opt/idris2" && \
59+
cd /build/idris && \
60+
idris2 --build echidna-validator.ipkg || true
61+
62+
# =============================================================================
63+
# Stage 3: Prover Installer
64+
# =============================================================================
65+
FROM cgr.dev/chainguard/wolfi-base:latest AS prover-installer
66+
67+
RUN apk add --no-cache \
68+
z3 \
69+
curl \
70+
ca-certificates
71+
72+
# Install Lean 4 via elan
73+
RUN curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | \
74+
sh -s -- -y --default-toolchain stable && \
75+
. "$HOME/.elan/env" && \
76+
lean --version
77+
78+
# =============================================================================
79+
# Stage 4: Runtime Image (Minimal, chainguard)
80+
# =============================================================================
81+
FROM cgr.dev/chainguard/wolfi-base:latest
82+
83+
LABEL maintainer="Jonathan D.A. Jewell <jonathan.jewell@open.ac.uk>"
84+
LABEL org.opencontainers.image.source="https://github.com/hyperpolymath/echidna"
85+
LABEL org.opencontainers.image.description="ECHIDNA - Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance"
86+
LABEL org.opencontainers.image.licenses="PMPL-1.0-or-later"
87+
LABEL org.opencontainers.image.version="1.5.0"
88+
LABEL org.opencontainers.image.vendor="hyperpolymath"
89+
90+
# Runtime dependencies only
91+
RUN apk add --no-cache \
92+
ca-certificates \
93+
libssl3 \
94+
gmp \
95+
z3
96+
97+
WORKDIR /app
98+
99+
# Copy echidna binary
100+
COPY --from=rust-builder /build/target/release/echidna /app/bin/echidna
101+
102+
# Copy Idris2 runtime (binary + prelude + base libs)
103+
COPY --from=idris2-builder /opt/idris2 /opt/idris2
104+
105+
# Copy echidna-validator if built
106+
COPY --from=idris2-builder /build/idris/build/exec/echidna-validator /app/bin/echidna-validator
107+
108+
# Copy Lean 4
109+
COPY --from=prover-installer /root/.elan /opt/elan
110+
111+
# Set up paths
112+
ENV PATH="/app/bin:/opt/idris2/bin:/opt/elan/toolchains/stable/bin:${PATH}"
113+
ENV IDRIS2_PREFIX="/opt/idris2"
114+
ENV ECHIDNA_PROVER_PATH="/opt"
115+
116+
# Create data directories
117+
RUN mkdir -p /app/proofs /app/config /app/logs
118+
119+
# Expose API port
120+
EXPOSE 8080
121+
122+
# Health check
123+
HEALTHCHECK --interval=30s --timeout=10s --start-period=5s --retries=3 \
124+
CMD ["/app/bin/echidna", "--version"]
125+
126+
ENTRYPOINT ["/app/bin/echidna"]
127+
CMD ["--help"]

‎.containerization/build.sh‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
#!/usr/bin/env bash
2+
# SPDX-License-Identifier: PMPL-1.0-or-later
3+
# Build ECHIDNA container images using Podman
4+
set -euo pipefail
5+
6+
SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
7+
REPO_ROOT="$(cd "$SCRIPT_DIR/.." && pwd)"
8+
IMAGE_NAME="${IMAGE_NAME:-echidna}"
9+
TAG="${TAG:-latest}"
10+
11+
build_minimal() {
12+
echo "Building minimal image: ${IMAGE_NAME}:${TAG}"
13+
podman build \
14+
-f "$SCRIPT_DIR/Containerfile" \
15+
-t "${IMAGE_NAME}:${TAG}" \
16+
"$REPO_ROOT"
17+
}
18+
19+
build_full() {
20+
echo "Building full image: ${IMAGE_NAME}:full"
21+
podman build \
22+
-f "$SCRIPT_DIR/Containerfile.full" \
23+
-t "${IMAGE_NAME}:full" \
24+
"$REPO_ROOT"
25+
}
26+
27+
case "${1:-minimal}" in
28+
minimal)
29+
build_minimal
30+
;;
31+
full)
32+
build_full
33+
;;
34+
all)
35+
build_minimal
36+
build_full
37+
;;
38+
*)
39+
echo "Usage: $0 {minimal|full|all}"
40+
exit 1
41+
;;
42+
esac

‎.github/workflows/ghcr-publish.yml‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -47,15 +47,20 @@ jobs:
4747
run: |
4848
echo "${{ secrets.GITHUB_TOKEN }}" | sudo nerdctl login ghcr.io -u ${{ github.actor }} --password-stdin
4949
50-
- name: Build image
50+
- name: Build minimal image
5151
run: |
52-
sudo nerdctl build -f Containerfile -t ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ github.sha }} .
52+
sudo nerdctl build -f .containerization/Containerfile -t ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ github.sha }} .
5353
sudo nerdctl tag ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ github.sha }} ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:latest
5454
55-
- name: Push image
55+
- name: Build full image
56+
run: |
57+
sudo nerdctl build -f .containerization/Containerfile.full -t ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:full .
58+
59+
- name: Push images
5660
run: |
5761
sudo nerdctl push ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ github.sha }}
5862
sudo nerdctl push ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:latest
63+
sudo nerdctl push ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:full
5964
6065
- name: Tag release version
6166
if: github.event_name == 'release'

‎.guix-channel‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
;; SPDX-License-Identifier: PMPL-1.0-or-later
2+
;; Guix channel definition for ECHIDNA
3+
(channel
4+
(version 0)
5+
(url "https://github.com/hyperpolymath/echidna")
6+
(name echidna))

‎.machine_readable/ECOSYSTEM.scm‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@
8787
((relationship . "backend-integration")
8888
(description . "Metamath minimal proof checker (tiny kernel)")
8989
(interaction . "Metamath database format")
90-
(url . "http://us.metamath.org")))
90+
(url . "https://us.metamath.org")))
9191

9292
(hol-light
9393
((relationship . "backend-integration")
@@ -99,7 +99,7 @@
9999
((relationship . "backend-integration")
100100
(description . "Mizar mathematical vernacular proof checker")
101101
(interaction . "Mizar article format")
102-
(url . "http://mizar.org")))
102+
(url . "https://mizar.org")))
103103

104104
(hol4
105105
((relationship . "backend-integration")
@@ -129,13 +129,13 @@
129129
((relationship . "backend-integration")
130130
(description . "Twelf logical framework (LF type theory)")
131131
(interaction . "Elf format")
132-
(url . "http://twelf.org")))
132+
(url . "https://twelf.org")))
133133

134134
(nuprl
135135
((relationship . "backend-integration")
136136
(description . "Nuprl constructive type theory prover")
137137
(interaction . "Nuprl proof format")
138-
(url . "http://www.nuprl.org")))
138+
(url . "https://www.nuprl.org")))
139139

140140
(minlog
141141
((relationship . "backend-integration")
@@ -228,7 +228,7 @@
228228
((relationship . "certificate-format")
229229
(description . "TSTP proof format for first-order ATPs")
230230
(usage . "Proof output from Vampire and E Prover")
231-
(url . "http://www.tptp.org/TSTP.html")))))
231+
(url . "https://www.tptp.org/TSTP.html")))))
232232

233233
(ml-frameworks
234234
((julia-ecosystem

‎Cargo.lock‎

Lines changed: 4 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

0 commit comments

Comments
 (0)