From 604d14b927bac6886c71360424b86acdcb7601fd Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 18 Nov 2025 20:53:26 +0000 Subject: [PATCH 1/3] Migrate from TravisCI to GitHub Actions - Create GitHub Actions workflow (.github/workflows/ci.yml) that preserves all functionality from .travis.yml - Update CI badges in README.md and README_ru.md to point to GitHub Actions - Maintain same build steps: system dependencies, tool installations (CVC4, OPAM, E-prover), OPAM package setup, and test execution - Use ubuntu-20.04 (similar to Travis bionic dist) and cache OPAM/bin directories for faster builds --- .github/workflows/ci.yml | 96 ++++++++++++++++++++++++++++++++++++++++ README.md | 2 +- README_ru.md | 2 +- 3 files changed, 98 insertions(+), 2 deletions(-) create mode 100644 .github/workflows/ci.yml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 0000000..7613021 --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,96 @@ +name: CI + +on: + push: + branches: [ main, master ] + pull_request: + branches: [ main, master ] + +jobs: + build: + runs-on: ubuntu-20.04 + + steps: + - uses: actions/checkout@v3 + + - name: Cache opam and binaries + uses: actions/cache@v3 + with: + path: | + ~/.opam + ~/bin + key: ${{ runner.os }}-opam-${{ hashFiles('**/*.opam') }} + restore-keys: | + ${{ runner.os }}-opam- + + - name: Install system dependencies + run: | + sudo apt-get update -qq + sudo apt-get install -y \ + aspcud \ + libgnomecanvas2-dev \ + libgtk2.0-dev \ + libgtksourceview2.0-dev \ + libgtk-3-dev \ + libgtksourceview-3.0-dev \ + z3 + + - name: Setup PATH and directories + run: | + mkdir -p $HOME/bin + echo "$HOME/bin" >> $GITHUB_PATH + + - name: Install CVC4 + run: | + if ! which cvc4; then + wget --quiet --no-clobber http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.7-x86_64-linux-opt \ + -O $HOME/bin/cvc4 + chmod +x $HOME/bin/cvc4 + fi + + - name: Install OPAM + run: | + if ! which opam; then + wget --quiet --no-clobber https://github.com/ocaml/opam/releases/download/2.0.8/opam-2.0.8-x86_64-linux \ + -O $HOME/bin/opam + chmod +x $HOME/bin/opam + fi + + - name: Install E-prover + run: | + if ! which eprover; then + wget https://github.com/eprover/eprover/archive/E-2.5.tar.gz + tar xzvf E-2.5.tar.gz + cd eprover-E-2.5 + ./configure --prefix=$HOME + make -j$(nproc) + sudo make install + fi + + - name: Initialize OPAM + run: | + opam init --auto-setup --disable-sandboxing --compiler=4.10.0 + opam install --yes depext + + - name: Install OPAM packages + run: | + opam repo add ispras https://forge.ispras.ru/git/astraver.opam-repository.git || true + opam update + opam upgrade --yes + opam depext --yes --noninteractive --install frama-c astraver why3 alt-ergo + rm -fr ~/.opam/log + + - name: Configure Why3 + run: | + eval $(opam env) + why3 config --detect + sed -i -e 's/running_provers_max = [[:digit:]]/running_provers_max = 1/' $HOME/.why3.conf + + - name: Run tests + run: | + eval $(opam env) + make run + make rte + make val + make sprove-proved-separatedly + make replay-proved-separatedly diff --git a/README.md b/README.md index 89e9f69..b2da5b1 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,5 @@ # VerKer -[![Replay Status](https://travis-ci.org/evdenis/verker.svg?branch=master)](https://travis-ci.org/evdenis/verker) +[![CI](https://github.com/evdenis/verker/actions/workflows/ci.yml/badge.svg)](https://github.com/evdenis/verker/actions/workflows/ci.yml) To view this file in Russian, please follow the [link](README_ru.md). diff --git a/README_ru.md b/README_ru.md index 6a3edb9..def0391 100644 --- a/README_ru.md +++ b/README_ru.md @@ -1,5 +1,5 @@ # VerKer -[![Replay Status](https://travis-ci.org/evdenis/verker.svg?branch=master)](https://travis-ci.org/evdenis/verker) +[![CI](https://github.com/evdenis/verker/actions/workflows/ci.yml/badge.svg)](https://github.com/evdenis/verker/actions/workflows/ci.yml) ACSL cпецификации к библиотечным функциям ядра Linux From bae04cfbe6210f6c8e4dc6f59188f2b81b0a8984 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 19 Nov 2025 09:43:55 +0000 Subject: [PATCH 2/3] Update GitHub Actions to use ubuntu-22.04 --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7613021..822bcdd 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -8,7 +8,7 @@ on: jobs: build: - runs-on: ubuntu-20.04 + runs-on: ubuntu-22.04 steps: - uses: actions/checkout@v3 From 28b2f9c973c118c72cb6bc4768cfde569e4a7e75 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 19 Nov 2025 09:46:07 +0000 Subject: [PATCH 3/3] Remove GTK packages not available in ubuntu-22.04 The GTK/GNOME libraries (libgnomecanvas2-dev, libgtk2.0-dev, libgtksourceview2.0-dev, libgtk-3-dev, libgtksourceview-3.0-dev) are not available or needed in ubuntu-22.04. These were likely dependencies for frama-c GUI, but CI uses command-line tools only. Keep only essential packages: aspcud (for opam) and z3 (theorem prover). --- .github/workflows/ci.yml | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 822bcdd..d3396e0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -26,14 +26,7 @@ jobs: - name: Install system dependencies run: | sudo apt-get update -qq - sudo apt-get install -y \ - aspcud \ - libgnomecanvas2-dev \ - libgtk2.0-dev \ - libgtksourceview2.0-dev \ - libgtk-3-dev \ - libgtksourceview-3.0-dev \ - z3 + sudo apt-get install -y aspcud z3 - name: Setup PATH and directories run: |