Skip to content

Commit

Permalink
more move
Browse files Browse the repository at this point in the history
  • Loading branch information
mtzguido committed Oct 26, 2024
1 parent 493f588 commit bb4d2ae
Show file tree
Hide file tree
Showing 7 changed files with 18 additions and 18 deletions.
6 changes: 3 additions & 3 deletions CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -152,14 +152,14 @@ examples. Alternatively, you can run `make -j test` from the Pulse root
directory, which will build Pulse beforehand.

If you have Docker, you can run `docker build -f
src/ci/opam.Dockerfile .` to test the opam installation of Pulse
ci/opam.Dockerfile .` to test the opam installation of Pulse
(including all dependencies.) This will also verify all examples and
tests, by moving them outside of the Pulse directory hierarchy
beforehand, to make sure that the location of those examples does not
need to depend on the location of Pulse.

Finally, you can run `make -j -C src ci` to re-extract, recompile and
Finally, you can run `make -j ci` to re-extract, recompile and
re-test everything. This rule also checks that the re-extracted
snapshot is no newer than the current snapshot. If you have Docker,
you can run the `ci` rule with `docker build -f src/ci/ci.Dockerfile
you can run the `ci` rule with `docker build -f ci/ci.Dockerfile
.` which will also install all dependencies automatically.
8 changes: 4 additions & 4 deletions ci/ci.Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -16,19 +16,19 @@ ARG opamthreads=24

# Install F* and Karamel from the Karamel CI install script
# FIXME: the `opam depext` command should be unnecessary with opam 2.1
ADD --chown=opam:opam src/ci/config.json pulse/src/ci/config.json
ADD --chown=opam:opam ci/config.json pulse/ci/config.json
ENV FSTAR_HOME=$HOME/FStar
ENV KRML_HOME=$HOME/karamel
RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends \
wget \
jq \
&& \
git clone --branch $(jq -c -r '.RepoVersions.fstar' pulse/src/ci/config.json || echo master) https://github.com/FStarLang/FStar $FSTAR_HOME && \
git clone --branch $(jq -c -r '.RepoVersions.fstar' pulse/ci/config.json || echo master) https://github.com/FStarLang/FStar $FSTAR_HOME && \
eval $(opam env) && \
opam depext conf-gmp z3.4.8.5-1 conf-m4 && \
opam install --deps-only $FSTAR_HOME/fstar.opam && \
env OTHERFLAGS='--admit_smt_queries true' make -C $FSTAR_HOME -j $opamthreads && \
git clone --branch $(jq -c -r '.RepoVersions.karamel' pulse/src/ci/config.json || echo master) https://github.com/FStarLang/karamel $KRML_HOME && \
git clone --branch $(jq -c -r '.RepoVersions.karamel' pulse/ci/config.json || echo master) https://github.com/FStarLang/karamel $KRML_HOME && \
eval $(opam env) && $KRML_HOME/.docker/build/install-other-deps.sh && \
env OTHERFLAGS='--admit_smt_queries true' make -C $KRML_HOME -j $opamthreads

Expand All @@ -46,6 +46,6 @@ RUN eval $(opam env) && \
ADD --chown=opam:opam ./ pulse/
ARG PULSE_NIGHTLY_CI
ARG OTHERFLAGS
RUN eval $(opam env) && . $HOME/.cargo/env && env PULSE_NIGHTLY_CI="$PULSE_NIGHTLY_CI" make -k -j $opamthreads -C pulse/src ci
RUN eval $(opam env) && . $HOME/.cargo/env && env PULSE_NIGHTLY_CI="$PULSE_NIGHTLY_CI" make -k -j $opamthreads -C pulse ci

ENV PULSE_HOME $HOME/pulse
4 changes: 2 additions & 2 deletions ci/hierarchic.Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,13 @@ ARG opamthreads=24
# Install Karamel
ENV KRML_HOME $HOME/pulse_tools/karamel
RUN mkdir -p $HOME/pulse_tools && \
git clone --branch $(jq -c -r '.RepoVersions.karamel' $HOME/pulse/src/ci/config.json || echo master) https://github.com/FStarLang/karamel $KRML_HOME && \
git clone --branch $(jq -c -r '.RepoVersions.karamel' $HOME/pulse/ci/config.json || echo master) https://github.com/FStarLang/karamel $KRML_HOME && \
eval $(opam env) && $KRML_HOME/.docker/build/install-other-deps.sh && \
env OTHERFLAGS='--admit_smt_queries true' make -C $KRML_HOME -j $opamthreads

# Pulse CI proper
ARG PULSE_NIGHTLY_CI
ARG OTHERFLAGS
RUN eval $(opam env) && . "$HOME/.cargo/env" && env PULSE_NIGHTLY_CI="$PULSE_NIGHTLY_CI" make -k -j $opamthreads -C $HOME/pulse/src ci
RUN eval $(opam env) && . "$HOME/.cargo/env" && env PULSE_NIGHTLY_CI="$PULSE_NIGHTLY_CI" make -k -j $opamthreads -C $HOME/pulse ci

ENV PULSE_HOME $HOME/pulse
6 changes: 3 additions & 3 deletions ci/no-fstar-home.Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -26,12 +26,12 @@ ENV KRML_HOME=$HOME/karamel
RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends \
jq \
&& \
git clone --branch $(jq -c -r '.RepoVersions.fstar' pulse/src/ci/config.json || echo master) https://github.com/FStarLang/FStar $HOME/FStar && \
git clone --branch $(jq -c -r '.RepoVersions.fstar' pulse/ci/config.json || echo master) https://github.com/FStarLang/FStar $HOME/FStar && \
eval $(opam env) && \
opam depext conf-gmp z3.4.8.5-1 conf-m4 && \
opam install --deps-only $HOME/FStar/fstar.opam && \
env OTHERFLAGS='--admit_smt_queries true' make -C $HOME/FStar -j $opamthreads && \
git clone --branch $(jq -c -r '.RepoVersions.karamel' pulse/src/ci/config.json || echo master) https://github.com/FStarLang/karamel $KRML_HOME && \
git clone --branch $(jq -c -r '.RepoVersions.karamel' pulse/ci/config.json || echo master) https://github.com/FStarLang/karamel $KRML_HOME && \
eval $(opam env) && $KRML_HOME/.docker/build/install-other-deps.sh && \
env FSTAR_HOME=$HOME/FStar OTHERFLAGS='--admit_smt_queries true' make -C $KRML_HOME -j $opamthreads

Expand All @@ -40,4 +40,4 @@ ENV PATH=$HOME/FStar/bin:$PATH
# Pulse CI proper
ARG PULSE_NIGHTLY_CI
ARG OTHERFLAGS
RUN eval $(opam env) && . "$HOME/.cargo/env" && env PULSE_NIGHTLY_CI="$PULSE_NIGHTLY_CI" make -k -j $opamthreads -C pulse/src ci
RUN eval $(opam env) && . "$HOME/.cargo/env" && env PULSE_NIGHTLY_CI="$PULSE_NIGHTLY_CI" make -k -j $opamthreads -C pulse ci
2 changes: 1 addition & 1 deletion ci/opam.Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ ADD --chown=opam:opam ./ pulse/
RUN sudo apt-get update && \
sudo apt-get install --yes --no-install-recommends jq && \
opam depext conf-gmp z3.4.8.5-1 conf-m4 && \
git clone --branch $(jq -c -r '.RepoVersions.fstar' pulse/src/ci/config.json || echo master) https://github.com/FStarLang/FStar FStar && \
git clone --branch $(jq -c -r '.RepoVersions.fstar' pulse/ci/config.json || echo master) https://github.com/FStarLang/FStar FStar && \
opam install -j $opamthreads -v -v -v FStar/fstar.opam && \
rm -rf FStar

Expand Down
6 changes: 3 additions & 3 deletions ci/package.Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -37,12 +37,12 @@ RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends \
wget \
jq \
&& \
git clone --branch $(jq -c -r '.RepoVersions.fstar' pulse/src/ci/config.json || echo master) https://github.com/FStarLang/FStar $FSTAR_HOME && \
git clone --branch $(jq -c -r '.RepoVersions.fstar' pulse/ci/config.json || echo master) https://github.com/FStarLang/FStar $FSTAR_HOME && \
eval $(opam env) && \
opam depext conf-gmp z3.4.8.5-1 conf-m4 && \
opam install --deps-only $FSTAR_HOME/fstar.opam && \
env OTHERFLAGS='--admit_smt_queries true' make -C $FSTAR_HOME -j $opamthreads && \
git clone --branch $(jq -c -r '.RepoVersions.karamel' pulse/src/ci/config.json || echo master) https://github.com/FStarLang/karamel $KRML_HOME && \
git clone --branch $(jq -c -r '.RepoVersions.karamel' pulse/ci/config.json || echo master) https://github.com/FStarLang/karamel $KRML_HOME && \
eval $(opam env) && $KRML_HOME/.docker/build/install-other-deps.sh && \
env OTHERFLAGS='--admit_smt_queries true' make -C $KRML_HOME -j $opamthreads

Expand All @@ -57,6 +57,6 @@ RUN eval $(opam env) && \
env OTHERFLAGS='--admit_smt_queries true' make -C $FSTAR_HOME -j $opamthreads bootstrap

# Produce the binary package
RUN eval $(opam env) && . $HOME/.cargo/env && pulse/src/ci/package.sh -j $opamthreads
RUN eval $(opam env) && . $HOME/.cargo/env && pulse/ci/package.sh -j $opamthreads

ENV PULSE_HOME $HOME/pulse
4 changes: 2 additions & 2 deletions ci/package.sh
Original file line number Diff line number Diff line change
Expand Up @@ -61,8 +61,8 @@ $cp -r $KRML_HOME/krmllib $fstar_package_dir/
$cp -r $KRML_HOME/include $fstar_package_dir/
$cp -r $KRML_HOME/misc $fstar_package_dir/

# assume current directory is $PULSE_HOME/src/ci
export PULSE_HOME=$(fixpath $(cd ../.. && pwd))
# assume current directory is $PULSE_HOME/ci
export PULSE_HOME=$(fixpath $(cd .. && pwd))

# use the package to build Pulse
export FSTAR_HOME="$fstar_package_dir"
Expand Down

0 comments on commit bb4d2ae

Please sign in to comment.