Earthfile

VERSION 0.8

theories:
    FROM coqorg/coq
    USER coq
    COPY --chown=coq lazy-wspace/theories /home/coq/lazy-wspace/theories
    COPY --chown=coq lazy-wspace/_CoqProject lazy-wspace/Makefile /home/coq/lazy-wspace
    WORKDIR /home/coq/lazy-wspace
    # TODO: BUG? With Docker this can just be `make`, but Earthly seems to
    # require it to be run as a login shell.
    RUN sh -lc make

build:
    FROM rust:1.76
    WORKDIR /lazy-wspace
    COPY lazy-wspace .
    # Exclude package wspace-syntax-test, because it requires GHC for comparing
    # against Haskell behavior. TODO: Enable it.
    RUN cargo test --package lazy-wspace \
                   --package lazy-wspace-macros \
                   --package wspace-syntax && \
        RUSTFLAGS='-C target-feature=+crt-static' cargo build --release --target x86_64-unknown-linux-gnu
    SAVE ARTIFACT target/x86_64-unknown-linux-gnu/release/compile /bin/
    SAVE ARTIFACT target/x86_64-unknown-linux-gnu/release/wspace /bin/
    SAVE ARTIFACT target/x86_64-unknown-linux-gnu/release/wspace-syntax /bin/
    SAVE ARTIFACT tests /programs
    BUILD +theories

docker:
    FROM scratch
    COPY +build/ /
    ENTRYPOINT ["/bin/compile"]
    SAVE IMAGE wspace-corpus/rust/thaliaarchi-lazy-wspace