Skip to content

Commit 69bf2a7

Browse files
distephdisteph
authored
Add CI harness (#9)
* Add GitHub CI with Windows JNI harness * Fix GitHub CI checkout and Yices pin * Include gmaketest in Yices sparse checkout * Update JNI status constants for Yices 2.7 * Align Java value tags with Yices 2.7 * Allow null parameters in context checks * Fix Windows Yices dist path detection * Update Windows JNI status constants for Yices 2.7 * Align Windows JNI and constructors with Yices 2.7 * Add Windows JNI context check exports * Complete Windows JNI parity with Unix bindings * Enable Yices 2.6.4 features in Windows JNI * Bound thread stress test in CI * Use deterministic CI test baseline
1 parent 95a7181 commit 69bf2a7

13 files changed

Lines changed: 877 additions & 97 deletions

File tree

‎.github/workflows/ci.yml‎

Lines changed: 146 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,146 @@
1+
name: CI
2+
3+
on:
4+
pull_request:
5+
push:
6+
7+
permissions:
8+
contents: read
9+
10+
env:
11+
FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: "true"
12+
YICES_REF: yices-2.7.0
13+
14+
jobs:
15+
unix:
16+
name: ${{ matrix.os }}
17+
runs-on: ${{ matrix.os }}
18+
strategy:
19+
fail-fast: false
20+
matrix:
21+
os:
22+
- ubuntu-latest
23+
- macos-latest
24+
25+
steps:
26+
- uses: actions/checkout@v5
27+
28+
- name: Checkout Yices
29+
uses: actions/checkout@v5
30+
with:
31+
repository: SRI-CSL/yices2
32+
ref: ${{ env.YICES_REF }}
33+
path: y2
34+
fetch-depth: 1
35+
sparse-checkout: |
36+
Makefile
37+
Makefile.build
38+
configure
39+
configure.ac
40+
config.guess
41+
config.sub
42+
gmaketest
43+
install-sh
44+
make.include.in
45+
autoconf
46+
configs
47+
scripts
48+
src
49+
utils
50+
sparse-checkout-cone-mode: false
51+
52+
- name: Set up Java
53+
uses: actions/setup-java@v5
54+
with:
55+
distribution: temurin
56+
java-version: "17"
57+
58+
- name: Install Linux dependencies
59+
if: runner.os == 'Linux'
60+
run: |
61+
sudo apt-get update
62+
sudo apt-get install -y ant autoconf automake g++ gcc gperf libgmp-dev libtool m4 make pkg-config
63+
64+
- name: Install macOS dependencies
65+
if: runner.os == 'macOS'
66+
env:
67+
HOMEBREW_NO_AUTO_UPDATE: "1"
68+
run: |
69+
brew install ant autoconf automake gmp gperf libtool make pkg-config
70+
71+
- name: Build and test
72+
env:
73+
YICES_SRC: ${{ github.workspace }}/y2
74+
YICES_PREFIX: ${{ runner.temp }}/yices-install
75+
run: bash scripts/ci-build-test-unix.sh
76+
77+
windows:
78+
name: windows-latest
79+
runs-on: windows-latest
80+
81+
steps:
82+
- run: git config --system core.longpaths true
83+
84+
- run: git config --global core.autocrlf false && git config --global core.eol lf
85+
86+
- uses: actions/checkout@v5
87+
88+
- name: Checkout Yices
89+
uses: actions/checkout@v5
90+
with:
91+
repository: SRI-CSL/yices2
92+
ref: ${{ env.YICES_REF }}
93+
path: y2
94+
fetch-depth: 1
95+
sparse-checkout: |
96+
Makefile
97+
Makefile.build
98+
configure
99+
configure.ac
100+
config.guess
101+
config.sub
102+
gmaketest
103+
install-sh
104+
make.include.in
105+
autoconf
106+
configs
107+
scripts
108+
src
109+
utils
110+
sparse-checkout-cone-mode: false
111+
112+
- name: Set up Java
113+
uses: actions/setup-java@v5
114+
with:
115+
distribution: temurin
116+
java-version: "17"
117+
118+
- name: Install Ant
119+
shell: powershell
120+
run: choco install ant -y
121+
122+
- name: Install Cygwin dependencies
123+
uses: cygwin/cygwin-install-action@v4
124+
with:
125+
packages: |
126+
autoconf,
127+
automake,
128+
cmake,
129+
coreutils,
130+
curl,
131+
gperf,
132+
libtool,
133+
m4,
134+
make,
135+
mingw64-x86_64-gcc-core,
136+
mingw64-x86_64-gcc-g++,
137+
moreutils,
138+
wget
139+
140+
- name: Build and test
141+
shell: bash
142+
env:
143+
CYGWIN: winsymlinks:native binmode
144+
YICES_SRC: ${{ github.workspace }}/y2
145+
YICES_PREFIX: /tmp/yices-install
146+
run: bash scripts/ci-build-test-windows.sh

‎ant.sh‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,15 @@
11
#!/bin/bash
22

33
#uses the build.sh to mimic what 'ant install' does without 'ant'
4+
set -e
5+
46
REPO_ROOT=${PWD}
57

68
YC=${REPO_ROOT}/build/classes
79
YI=${REPO_ROOT}/dist/lib
810

911
YICES_CLASSPATH=${YC} YICES_JNI=${YI} ./build.sh
1012

11-
jar -cvfm ${YI}/yices.jar ${REPO_ROOT}/MANIFEST.txt -C ${YC} ${YC}/com/sri/yices/*.class
13+
jar -cvfm ${YI}/yices.jar ${REPO_ROOT}/MANIFEST.txt -C ${YC} .
1214

1315
java -Djava.library.path=${REPO_ROOT}/dist/lib -jar ${REPO_ROOT}/dist/lib/yices.jar

‎build.xml‎

Lines changed: 26 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -223,7 +223,7 @@
223223
<echo> Executing "make ${library}" in ${code} </echo>
224224
<exec executable="make"
225225
dir="${code}"
226-
failifexecutionfails="true">
226+
failonerror="true">
227227
<arg line="${library}"/>
228228
</exec>
229229

@@ -233,7 +233,7 @@
233233

234234
<exec executable="make"
235235
dir="${code}"
236-
failifexecutionfails="true">
236+
failonerror="true">
237237
<arg line="install"/>
238238
</exec>
239239

@@ -250,7 +250,7 @@
250250

251251
<exec executable="make"
252252
dir="${code}"
253-
failifexecutionfails="true">
253+
failonerror="true">
254254
<arg line="clean"/>
255255
</exec>
256256
</target>
@@ -286,12 +286,35 @@
286286
<test name="com.sri.yices.TestTypes"/>
287287
<test name="com.sri.yices.TestYices"/>
288288
<test name="com.sri.yices.TestModels"/>
289+
<test name="com.sri.yices.TestTermComponents"/>
289290
<!-- <test name="com.sri.yices.TestDelegates"/> -->
290291
<!-- <test name="com.sri.yices.TestDimacs"/> -->
291292
<test name="com.sri.yices.TestThreads"/>
292293
</junit>
293294
</target>
294295

296+
<target name="ci-test" depends="dist,test-compile,install">
297+
<echo> Running CI tests </echo>
298+
<echo> test_classes: ${test_classes} </echo>
299+
<echo> java.library.path: ${java.library.path} </echo>
300+
<junit printsummary="on" haltonfailure="yes" fork="true">
301+
<sysproperty key="java.library.path" path="${jnilib}"/>
302+
<classpath>
303+
<path refid="classpath.test"/>
304+
<pathelement location="${test_classes}"/>
305+
</classpath>
306+
<formatter type="brief" usefile="false" />
307+
<test name="com.sri.yices.TestBigRationals"/>
308+
<test name="com.sri.yices.TestConstructor"/>
309+
<test name="com.sri.yices.TestContext"/>
310+
<test name="com.sri.yices.TestStatus"/>
311+
<test name="com.sri.yices.TestTypes"/>
312+
<test name="com.sri.yices.TestYices"/>
313+
<test name="com.sri.yices.TestModels"/>
314+
<test name="com.sri.yices.TestTermComponents"/>
315+
</junit>
316+
</target>
317+
295318
<path id="classpath.examples">
296319
<pathelement location="${dist}/lib/yices.jar"/>
297320
<pathelement location="examples"/>

‎scripts/ci-build-test-unix.sh‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
#!/usr/bin/env bash
2+
3+
set -euo pipefail
4+
5+
REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
6+
YICES_SRC="${YICES_SRC:?set YICES_SRC}"
7+
YICES_PREFIX="${YICES_PREFIX:?set YICES_PREFIX}"
8+
9+
configure_brew_env() {
10+
if [[ "$(uname)" != "Darwin" ]]; then
11+
return
12+
fi
13+
14+
local brew_prefix
15+
if [[ -d /opt/homebrew ]]; then
16+
brew_prefix=/opt/homebrew
17+
else
18+
brew_prefix=/usr/local
19+
fi
20+
21+
export CPPFLAGS="-I${brew_prefix}/include ${CPPFLAGS:-}"
22+
export LDFLAGS="-L${brew_prefix}/lib ${LDFLAGS:-}"
23+
export PKG_CONFIG_PATH="${brew_prefix}/lib/pkgconfig${PKG_CONFIG_PATH:+:${PKG_CONFIG_PATH}}"
24+
export DYLD_LIBRARY_PATH="${brew_prefix}/lib${DYLD_LIBRARY_PATH:+:${DYLD_LIBRARY_PATH}}"
25+
}
26+
27+
build_yices() {
28+
rm -rf "${YICES_PREFIX}"
29+
mkdir -p "${YICES_PREFIX}"
30+
pushd "${YICES_SRC}" >/dev/null
31+
autoconf
32+
./configure --prefix="${YICES_PREFIX}" --enable-thread-safety --disable-mcsat
33+
make MODE=release
34+
make MODE=release install
35+
popd >/dev/null
36+
}
37+
38+
run_java_ci() {
39+
export CPPFLAGS="-I${YICES_PREFIX}/include ${CPPFLAGS:-}"
40+
export LDFLAGS="-L${YICES_PREFIX}/lib ${LDFLAGS:-}"
41+
42+
if [[ "$(uname)" == "Darwin" ]]; then
43+
export DYLD_LIBRARY_PATH="${YICES_PREFIX}/lib${DYLD_LIBRARY_PATH:+:${DYLD_LIBRARY_PATH}}"
44+
else
45+
export LD_LIBRARY_PATH="${YICES_PREFIX}/lib${LD_LIBRARY_PATH:+:${LD_LIBRARY_PATH}}"
46+
fi
47+
48+
export YICES_JNI="${REPO_ROOT}/dist/lib"
49+
export YICES_CLASSPATH="${REPO_ROOT}/build/classes"
50+
51+
pushd "${REPO_ROOT}" >/dev/null
52+
ant clean ci-test
53+
popd >/dev/null
54+
}
55+
56+
configure_brew_env
57+
build_yices
58+
run_java_ci

0 commit comments

Comments
 (0)