Skip to content

CI: ebmc-packages workflow fixes #539

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

Merged
merged 1 commit into from
Jun 12, 2024
Merged
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
80 changes: 79 additions & 1 deletion .github/workflows/ebmc-packages.yaml
Original file line number Diff line number Diff line change
@@ -1,10 +1,11 @@
on:
release:
types: [created]
types: [published]
Comment on lines 1 to +3
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it would be better to use tags as the trigger, else you end up publishing a release but don't yet have artifacts in place at the time of publication (and instead hope for them to be created soonish). See https://github.com/model-checking/kani/blob/main/.github/workflows/release.yml#L8-L15 for triggers that appear to work well for us.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, will change once this flow works.


name: Upload additional release assets
jobs:
ubuntu-22_04-package:
name: Ubuntu 22.04
runs-on: ubuntu-22.04
steps:
- uses: actions/checkout@v4
Expand Down Expand Up @@ -69,3 +70,80 @@ jobs:
asset_path: ${{ steps.create_packages.outputs.deb_package }}
asset_name: ${{ steps.create_packages.outputs.deb_package_name }}
asset_content_type: application/x-deb

centos8-package:
name: CentOS 8
runs-on: ubuntu-22.04
container:
image: centos:8
steps:
- name: Install Packages
run: |
sed -i -e "s|mirrorlist=|#mirrorlist=|g" -e "s|#baseurl=http://mirror.centos.org|baseurl=http://vault.centos.org|g" /etc/yum.repos.d/CentOS-Linux-*
yum -y install make gcc-c++ flex bison git rpmdevtools wget
wget --no-verbose https://github.com/ccache/ccache/releases/download/v4.8.3/ccache-4.8.3-linux-x86_64.tar.xz
tar xJf ccache-4.8.3-linux-x86_64.tar.xz
cp ccache-4.8.3-linux-x86_64/ccache /usr/bin/
- name: cache for ccache
uses: actions/cache@v4
with:
path: /github/home/.cache/ccache
save-always: true
key: ${{ runner.os }}-centos8-make-gcc-${{ github.ref }}-${{ github.sha }}-PR
restore-keys: ${{ runner.os }}-centos8-make-gcc-
- uses: actions/checkout@v4
with:
submodules: recursive
- name: Zero ccache stats and limit in size
run: ccache -z --max-size=500M
- name: ccache path
run: ccache -p | grep cache_dir
- name: Get minisat
run: make -C lib/cbmc/src minisat2-download
- name: Build with make
run: make CXX="ccache g++ -Wno-class-memaccess" LIBS="-lstdc++fs" -C src -j2
- name: Run the ebmc tests with SAT
run: |
rm regression/ebmc/neural-liveness/counter1.desc
make -C regression/ebmc test
- name: Run the verilog tests
run: make -C regression/verilog test
- name: Create .rpm
run |
VERSION=$(echo ${{ github.ref }} | cut -d "/" -f 3 | cut -d "-" -f 2)
rpmdev-setuptree

cat > ~/rpmbuild/SPECS/ebmc.spec << EOM
#This is a spec file for ebmc

Summary: EBMC Model Checker
License: BSD 3-clause
Name: ebmc
Version: ${VERSION}
Release: 1
Prefix: /usr
Group: Development/Tools
Requires:

%description
EBMC is a formal verification tool for hardware designs.

%prep

%build

%install
mkdir %{buildroot}/usr
mkdir %{buildroot}/usr/lib
mkdir %{buildroot}/usr/bin
mkdir %{buildroot}/usr/lib/ebmc
cp ${SRC}/src/ebmc/jcover %{buildroot}/usr/bin/

%files
/usr/bin/ebmc
EOM

echo Building ebmc-${VERSION}-1.x86_64.rpm
(cd ~/rpmbuild/SPECS ; rpmbuild -v -bb ebmc.spec )
- name: Print ccache stats
run: ccache -s