Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Convert Lakeroad to Churchroad #2

Merged
merged 10 commits into from
Feb 16, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 12 additions & 27 deletions .github/workflows/run-checks-github-runners.yml
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
name: Run checks
name: Build Docker image, format check, and run tests

on:
push:
Expand Down Expand Up @@ -34,11 +34,11 @@ jobs:
#
# TODO(@gussmith23) It would be nice if this wasn't necessary. We could use
# this: https://docs.github.com/en/actions/hosting-your-own-runners/running-scripts-before-or-after-a-job
cleaner:
runs-on: self-hosted
steps:
- name: Clean up previous runs
run: rm -rf "${{ github.workspace }}"
# cleaner:
# runs-on: self-hosted
# steps:
# - name: Clean up previous runs
# run: rm -rf "${{ github.workspace }}"

build-and-push-image:
runs-on: ubuntu-latest
Expand All @@ -47,15 +47,8 @@ jobs:
packages: write

steps:
# Set up SSH agent for cloning lakeroad-private.
- uses: webfactory/[email protected]
with:
ssh-private-key: ${{ secrets.LAKEROAD_PRIVATE_SSH_KEY }}

- name: Checkout repository
uses: actions/checkout@v3
with:
submodules: true

- name: Log in to the Container registry
uses: docker/login-action@v2
Expand Down Expand Up @@ -84,15 +77,12 @@ jobs:
cache-from: type=gha
no-cache: ${{ github.event.inputs.no-cache == 'true' }}

# This can be run on ubuntu-latest (i.e., on GitHub's provided runners), but
# it will be much slower. Specifically, our end-to-end tests using Verilator
# take advantage of the many threads on our machines, whereas the GitHub
# machines only have two threads.
#
# Perhaps we should run this on both?
run-tests:
runs-on: self-hosted
needs: [build-and-push-image, cleaner]
runs-on: ubuntu-latest
needs: [build-and-push-image,
# Needed if we switch back to self-hosted.
# cleaner,
]
steps:
- name: Log in to the Container registry
uses: docker/login-action@v2
Expand Down Expand Up @@ -121,10 +111,5 @@ jobs:
- name: Pull image
run: docker pull ${{ env.IMAGE_TAG }}

- name: Racket format check
run: |
docker run ${{ env.IMAGE_TAG }} \
bash -c 'raco fmt -i racket/*.rkt && git diff && [ -z "$(git status --porcelain)" ]'

- name: Rust format check
run: docker run ${{ env.IMAGE_TAG }} cargo fmt --manifest-path ./rust/Cargo.toml -- --check
run: docker run ${{ env.IMAGE_TAG }} cargo fmt --manifest-path ./Cargo.toml -- --check
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -9,3 +9,6 @@
**/.lit_test_times.txt
**/Output/
**/__pycache__

target
Cargo.lock
5 changes: 1 addition & 4 deletions .gitmodules
Original file line number Diff line number Diff line change
@@ -1,6 +1,3 @@
[submodule "lakeroad-private"]
path = lakeroad-private
url = [email protected]:uwsampl/lakeroad-private
[submodule "lakeroad-egglog/yosys"]
path = lakeroad-egglog/yosys
path = yosys
url = [email protected]:uwsampl/yosys
2 changes: 1 addition & 1 deletion lakeroad-egglog/Cargo.toml → Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
[package]
name = "lakeroad-egglog"
name = "churchroad"
version = "0.1.0"
edition = "2021"

Expand Down
152 changes: 12 additions & 140 deletions Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,9 @@ FROM ubuntu:22.04
ARG MAKE_JOBS=2
SHELL ["/bin/bash", "-c"]

# Update, get add-apt-repository, add PPA for Racket, update again.
# Update, get add-apt-repository.
RUN apt update \
&& apt install -y software-properties-common \
&& add-apt-repository ppa:plt/racket \
&& apt update
&& apt install -y software-properties-common

# Install apt dependencies
# `noninteractive` prevents the tzdata package from asking for a timezone on the
Expand Down Expand Up @@ -49,150 +47,24 @@ RUN apt install -y \
zlib1g \
zlib1g-dev

# Point to llvm-config binary. Alternatively, make sure you have a binary called
# `llvm-config` on your PATH.
ENV LLVM_CONFIG=llvm-config-14

# Make a binary for `lit`. If you're on Mac, you can install lit via Brew.
# Ubuntu doesn't have a binary for it, but it is available on pip and is
# installed later in this Dockerfile.
WORKDIR /root
RUN mkdir -p /root/.local/bin \
&& echo "#!/usr/bin/env python3" >> /root/.local/bin/lit \
&& echo "from lit.main import main" >> /root/.local/bin/lit \
&& echo "if __name__ == '__main__': main()" >> /root/.local/bin/lit \
&& chmod +x /root/.local/bin/lit
ENV PATH="/root/.local/bin:${PATH}"

# Install a bunch of useful tools from prebuilt binaries. Thanks to YosysHQ for
# making this available!
#
# If we get an error here, we likely just need to add other branches for other
# architectures.
#
# TODO(@gussmith23): Could shrink Docker image by deleting a bunch of uneeded
# binaries, or only taking the binaries we need. However, I found that moving
# stuff out of oss-cad-suite causes things to break.
WORKDIR /root
ADD dependencies.sh /root/dependencies.sh
RUN source /root/dependencies.sh \
&& if [ "$(uname -m)" = "x86_64" ] ; then \
wget https://github.com/YosysHQ/oss-cad-suite-build/releases/download/$OSS_CAD_SUITE_DATE/oss-cad-suite-linux-x64-$(echo $OSS_CAD_SUITE_DATE | tr -d "-").tgz -q -O oss-cad-suite.tgz; \
else \
exit 1; \
fi \
&& tar xf oss-cad-suite.tgz \
&& rm oss-cad-suite.tgz \
# Delete binaries we don't need (and that we explicitly build other versions
# of).
&& rm oss-cad-suite/bin/yosys \
&& rm oss-cad-suite/bin/bitwuzla
# Make sure that .local/bin has precedence over oss-cad-suite/bin. I realize
# we add ./local/bin to the PATH twice, but I just want to document that we want
# things in .local/bin to take precedence, and duplicate PATH entries won't
# break anything.
ENV PATH="/root/.local/bin:/root/oss-cad-suite/bin:${PATH}"

# pip dependencies
WORKDIR /root/lakeroad
ADD requirements.txt requirements.txt
RUN pip install -r requirements.txt

# Build Bitwuzla.
WORKDIR /root
RUN source /root/dependencies.sh \
&& mkdir bitwuzla \
&& wget -qO- https://github.com/bitwuzla/bitwuzla/archive/$BITWUZLA_COMMIT_HASH.tar.gz | tar xz -C bitwuzla --strip-components=1 \
&& cd bitwuzla \
&& ./configure.py --prefix=/root/.local \
&& cd build \
&& ninja -j${MAKE_JOBS} \
&& ninja install \
&& rm -rf /root/bitwuzla

# Install raco (Racket) dependencies.
WORKDIR /root
RUN \
# First, fix https://github.com/racket/racket/issues/2691 by building the
# docs.
raco setup --doc-index --force-user-docs \
# Install packages.
&& raco pkg install --deps search-auto --batch \
rosette \
yaml \
# Install fmt directly from GitHub. This prevents the version from changing on
# us unexpectedly.
&& cd /root \
&& git clone https://github.com/sorawee/fmt \
&& cd fmt \
&& source /root/dependencies.sh \
&& git checkout $RACKET_FMT_COMMIT_HASH \
&& raco pkg install --deps search-auto --batch

# Install Rust
RUN curl https://sh.rustup.rs -sSf | sh -s -- -y
ENV PATH="/root/.cargo/bin:$PATH"

ENV LAKEROAD_DIR=/root/lakeroad
ENV PYTHONPATH="${LAKEROAD_DIR}/python:${PYTHONPATH}"

# Build Rust package.
WORKDIR /root/lakeroad
ADD ./rust ./rust
RUN cargo build --manifest-path /root/lakeroad/rust/Cargo.toml

# Add other Lakeroad files. It's useful to put this as far down as possible. In
# general, only ADD files just before they're needed. This maximizes the ability
# to cache intermediate containers and minimizes rebuilding.
# Add other Churchroad files. It's useful to put this as far down as possible.
# In general, only ADD files just before they're needed. This maximizes the
# ability to cache intermediate containers and minimizes rebuilding.
#
# In reality, we use the git functionality of ADD (enabled in our case via the
# optional flag --keep-git-dir) to add all of the checked-in files of the
# Lakeroad repo (but not including the .git directory itself). We could cut this
# down further if we wanted, but I think this is a clean approach for now.
WORKDIR /root/lakeroad
# Churchroad repo (but not including the .git directory itself). We could cut
# this down further if we wanted, but I think this is a clean approach for now.
WORKDIR /root/churchroad
ADD --keep-git-dir=false . .

# Build Racket bytecode; makes Lakeroad much faster.
RUN raco make /root/lakeroad/bin/main.rkt

# Point to lakeroad-private repo. This may or may not exist, if you didn't clone
# the lakeroad-private submodule. However, it shouldn't matter, as anything that
# uses LAKEROAD_PRIVATE_DIR should check if the directory exists/is nonempty first.
ENV LAKEROAD_PRIVATE_DIR=/root/lakeroad/lakeroad-private

# Build STP.
WORKDIR /root
RUN apt-get install -y git cmake bison flex libboost-all-dev python2 perl && \
source /root/dependencies.sh && \
mkdir stp && cd stp && \
wget -qO- https://github.com/stp/stp/archive/$STP_COMMIT_HASH.tar.gz | tar xz --strip-components=1 && \
./scripts/deps/setup-gtest.sh && \
./scripts/deps/setup-outputcheck.sh && \
./scripts/deps/setup-cms.sh && \
./scripts/deps/setup-minisat.sh && \
mkdir build && \
cd build && \
cmake .. -DCMAKE_INSTALL_PREFIX=/root/.local && \
make -j ${MAKE_JOBS}
# TODO(@gussmith23): Install and delete folder once
# https://github.com/stp/stp/issues/479 is fixed.
# make install && \
# rm -rf /root/stp
# And after that we also don't need to add STP to the path.
ENV PATH="/root/stp/build:${PATH}"

# Build Yosys.
WORKDIR /root
RUN source /root/dependencies.sh \
&& mkdir yosys && cd yosys \
&& wget -qO- https://github.com/YosysHQ/yosys/archive/$YOSYS_COMMIT_HASH.tar.gz | tar xz --strip-components=1 \
&& PREFIX="/root/.local" CPLUS_INCLUDE_PATH="/usr/include/tcl8.6/:$CPLUS_INCLUDE_PATH" make config-gcc \
&& PREFIX="/root/.local" CPLUS_INCLUDE_PATH="/usr/include/tcl8.6/:$CPLUS_INCLUDE_PATH" make -j ${MAKE_JOBS} install \
&& rm -rf /root/yosys

# Build Yosys plugin.
WORKDIR /root/lakeroad/yosys-plugin
RUN make -j ${MAKE_JOBS}
# Build Rust package.
WORKDIR /root/churchroad
RUN cargo build

WORKDIR /root/lakeroad
WORKDIR /root/churchroad
CMD [ "/bin/bash", "run-tests.sh" ]
Loading
Loading