Skip to content
Open

Nl2lin #8752

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1489 commits
Select commit Hold shift + click to select a range
ccaa346
update version
NikolajBjorner Feb 8, 2026
8672d26
remove obsoleted ADO workflows
NikolajBjorner Feb 8, 2026
29ad07c
version updated on workflows
NikolajBjorner Feb 8, 2026
1fa4304
remove redundant assert
nunoplopes Feb 8, 2026
70626ac
mpz: use pointer tagging to save space (#8447)
Copilot Feb 8, 2026
e73c897
constructor
nunoplopes Feb 8, 2026
3a8b688
Store rational by value in parameter variant (#8518)
Copilot Feb 8, 2026
62bfb13
Initial plan
Copilot Feb 8, 2026
d3c388a
Add -headerpad_max_install_names flag for macOS dylib builds
Copilot Feb 8, 2026
f0c3a5b
fix nlsat_explain.cpp that the regression tests would pass with lws=f…
levnach Feb 8, 2026
0761e91
Remove unused swap() methods (#8538)
Copilot Feb 8, 2026
3e54f23
Update RELEASE_NOTES.md for version 4.15.6
NikolajBjorner Feb 8, 2026
d245610
update version
NikolajBjorner Feb 8, 2026
5528eac
Initial plan
Copilot Feb 8, 2026
bde5553
Add macOS dylib headerpad validation to nightly and release workflows
Copilot Feb 8, 2026
2b3afe1
Add documentation for macOS headerpad validation
Copilot Feb 8, 2026
c291c7c
Fix install_name_tool command and runner consistency in validation jobs
Copilot Feb 8, 2026
3ae8d70
Apply headerpad fix to build systems (Python and CMake) and fix valid…
Copilot Feb 8, 2026
3c401f1
Fix CMake variable name and clarify test path documentation
Copilot Feb 8, 2026
51fd4b2
Fix OCaml linker flag and align validation runners with build runners
Copilot Feb 8, 2026
1387b2a
Delete .github/workflows/README-macos-headerpad.md
NikolajBjorner Feb 8, 2026
b670727
Initial plan
Copilot Feb 8, 2026
df02476
Remove OCaml Build badge from README status table
Copilot Feb 8, 2026
0be8dee
Revert "mpz: use pointer tagging to save space (#8447)"
NikolajBjorner Feb 8, 2026
4c43bf5
fix the logic of adding all coefficients and blocking double insertio…
levnach Feb 9, 2026
a7dbe16
update to next version
NikolajBjorner Feb 9, 2026
2aab748
update release
NikolajBjorner Feb 9, 2026
b8cfce9
update release
NikolajBjorner Feb 9, 2026
c50d41a
update readme with workflows
NikolajBjorner Feb 9, 2026
58431ec
Replace user-defined swap with C++11 move semantics for covert move p…
Copilot Feb 9, 2026
fc6355c
Update Windows.yml
NikolajBjorner Feb 9, 2026
b7bf23c
move, dont copy
nunoplopes Feb 9, 2026
bfc132a
move, dont copy
nunoplopes Feb 9, 2026
6b28d65
set random seed directly on m_smt_params before context initialization
NikolajBjorner Feb 9, 2026
a3e7bbb
replace some copies with moves
nunoplopes Feb 9, 2026
9152013
remove a few copies
nunoplopes Feb 10, 2026
bbb2991
fix crash
nunoplopes Feb 10, 2026
c8cd205
fix build warnings and scoop up after Nuno's leaks
NikolajBjorner Feb 10, 2026
06e6d55
Bump actions/download-artifact from 6.0.0 to 7.0.0
dependabot[bot] Feb 10, 2026
2e4a7c7
Bump github/gh-aw from 0.42.6 to 0.42.17
dependabot[bot] Feb 10, 2026
25b48a7
Bump githubnext/gh-aw from 0.40.0 to 0.42.17
dependabot[bot] Feb 10, 2026
23a0a52
revert swap changes to fix CI
nunoplopes Feb 10, 2026
dcd8ea4
fix build of test
NikolajBjorner Feb 10, 2026
ba0a332
Enhance nightly workflow to include Linux builds
NikolajBjorner Feb 10, 2026
426caf5
Initial plan
Copilot Feb 10, 2026
9cd53f1
Add a3-python agentic workflow
Copilot Feb 10, 2026
5400b39
Add README documentation for a3-python workflow
Copilot Feb 10, 2026
1e7be62
Delete .github/workflows/README-a3-python.md
NikolajBjorner Feb 10, 2026
62030bf
Simplify svector assignment operators using = default (#8566)
Copilot Feb 10, 2026
08eb25e
Add network permissions to Python workflow
NikolajBjorner Feb 10, 2026
972f90e
Initial plan
Copilot Feb 10, 2026
eef7d12
Recompile a3-python.md workflow with gh-aw v0.43.2
Copilot Feb 10, 2026
24f3cdd
relax a too strong assert
levnach Feb 10, 2026
05e8e4a
fix another regression by Nuno's changes
NikolajBjorner Feb 10, 2026
2a1be13
Initial plan
Copilot Feb 10, 2026
b739cd2
Fix YAML indentation in a3-python.md network field
Copilot Feb 10, 2026
6bdd035
update
NikolajBjorner Feb 10, 2026
88a2a82
fix #8552
NikolajBjorner Feb 11, 2026
e0f7c35
Update nightly.yml
NikolajBjorner Feb 11, 2026
6105a35
Initial plan
Copilot Feb 11, 2026
f4302f6
Add sparse-checkout step to a3-python workflow for Python source files
Copilot Feb 11, 2026
f334ba4
Add documentation for a3-python workflow fix
Copilot Feb 11, 2026
816b0d2
recompile aw
NikolajBjorner Feb 11, 2026
4183ed6
remove readmes
NikolajBjorner Feb 11, 2026
0644a25
v2 workflow
NikolajBjorner Feb 11, 2026
0749423
Add agentic workflow a3-python-v2
NikolajBjorner Feb 11, 2026
776976c
fix #8572
NikolajBjorner Feb 11, 2026
2247858
Update Linux binary handling in nightly workflow
NikolajBjorner Feb 11, 2026
2280cf4
publish test pypi
NikolajBjorner Feb 11, 2026
15af4b9
Rename publish-test.pypi to publish-test-pypi
NikolajBjorner Feb 11, 2026
f278f3d
Fix indentation for publish-test-pypi job
NikolajBjorner Feb 11, 2026
a163ace
fix underscore
NikolajBjorner Feb 11, 2026
1e53d52
Initial plan
Copilot Feb 11, 2026
867685a
Optimize a3-python-v2 workflow for better issue formatting
Copilot Feb 11, 2026
6d2619a
Recompile a3-python-v2 workflow with gh-aw v0.43.5
Copilot Feb 11, 2026
78d22dd
Initial plan
Copilot Feb 11, 2026
76fd385
Fix code-coverage workflow by adding --merge-mode-functions to gcovr …
Copilot Feb 11, 2026
9e489da
Initial plan
Copilot Feb 11, 2026
f2ad141
Refactor manylinux wheel production in nightly.yml workflow
Copilot Feb 11, 2026
f6f8bea
Remove copies (#8583)
nunoplopes Feb 11, 2026
bda8712
Initial plan
Copilot Feb 11, 2026
8fbf3f0
Fix manylinux-python-arm64 to use native ARM64 container via QEMU
Copilot Feb 11, 2026
730a54a
Eliminate unnecessary copy operations in function parameters and rang…
Copilot Feb 11, 2026
c031058
small update to testing on p.m_sls_worker instead of should_run_sls
NikolajBjorner Feb 12, 2026
07c639a
#8552
NikolajBjorner Feb 12, 2026
e8a8260
manual attempt to fix up how wheels are copied based on old release.y…
NikolajBjorner Feb 12, 2026
d9466be
revert back to working build for manylinux arm
NikolajBjorner Feb 12, 2026
803b71f
Initial plan
Copilot Feb 12, 2026
c946207
Fix BOUNDS and ASSERT_FAIL issues in Python API
Copilot Feb 12, 2026
4c8b540
Fix copy command for Linux Python packages
NikolajBjorner Feb 12, 2026
49d4127
Remove assertion for number of watches in normalize
NikolajBjorner Feb 12, 2026
8c78067
Add release trigger to documentation workflow
NikolajBjorner Feb 12, 2026
8fc8b51
Remove --clobber option from nightly release
NikolajBjorner Feb 12, 2026
5b54e41
bump version to prepare for release with wheels and npm
NikolajBjorner Feb 12, 2026
fa17a90
Initial plan
Copilot Feb 12, 2026
28db5e2
Fix 9 critical assert statements and RatVal division by zero (Priorit…
Copilot Feb 12, 2026
0ee04d2
Add comprehensive tests for Python API bug fixes
Copilot Feb 12, 2026
25c2b7e
Fix error message capitalization for Python conventions
Copilot Feb 12, 2026
bcc8797
Delete src/api/python/test_critical_fixes.py
NikolajBjorner Feb 12, 2026
487db1a
Modify behavior for division by zero
NikolajBjorner Feb 12, 2026
014ba14
Initial plan
Copilot Feb 12, 2026
9fe340c
Fix nightly build workflow by removing --clobber and adding deduplica…
Copilot Feb 12, 2026
86c2fa7
Improve file handling to properly handle special characters
Copilot Feb 12, 2026
d7f87d7
Add proper error handling for empty file list and preserve filepath i…
Copilot Feb 12, 2026
5fc2943
Fix EOF handling in bash read and improve empty content detection
Copilot Feb 12, 2026
ba75aae
Replace Python deduplication script with shell commands
Copilot Feb 12, 2026
fdb4a4d
update release to dedup and include manylinux
NikolajBjorner Feb 12, 2026
36342f9
increment minor version
NikolajBjorner Feb 13, 2026
8506195
Initial plan
Copilot Feb 12, 2026
4903917
Fix test-nuget on macOS by rewriting csproj with proper configuration
Copilot Feb 12, 2026
d75fbe7
Remove RuntimeIdentifier to fix assembly loading on macOS
Copilot Feb 12, 2026
61d8547
add tool
NikolajBjorner Feb 13, 2026
d9c6da2
Eliminate unnecessary copies with std::move for ref-counted types (#8…
Copilot Feb 13, 2026
adacc27
upgrade workflows
NikolajBjorner Feb 13, 2026
a03500a
git bindings v1.0
NikolajBjorner Feb 16, 2026
380a8ee
Alias ArithRef.__abs__ to Abs
danielzgtg Feb 14, 2026
5b349f8
Suggest eval in ModelRef.__getitem__ error
danielzgtg Feb 14, 2026
c281e9d
Add Solver.solutions(t)
danielzgtg Feb 15, 2026
a29b41c
Initial plan
Copilot Feb 13, 2026
068e8c7
Fix git sparse-checkout error in a3-python workflows
Copilot Feb 13, 2026
8ab445c
remove junk
NikolajBjorner Feb 16, 2026
06a49cd
Initial plan
Copilot Feb 16, 2026
5202b40
Fix a3-python-v2 workflow compilation error
Copilot Feb 16, 2026
c17e8f9
Document example for Solver.sexpr()
danielzgtg Feb 15, 2026
54b1232
Initial plan
Copilot Feb 16, 2026
3930647
Fix template interpolation failure in agentic workflows
Copilot Feb 16, 2026
7c01e5d
Initial plan
Copilot Feb 16, 2026
d414646
Add std::initializer_list overloads for update_quantifier and update …
Copilot Feb 16, 2026
fbda302
Initial plan
Copilot Feb 16, 2026
d958036
Add initializer_list overloads and update all call sites
Copilot Feb 16, 2026
6e91f3b
Add test for initializer_list overloads
Copilot Feb 16, 2026
eedade1
Restore defensive SASSERT in smt_conflict_resolution
Copilot Feb 16, 2026
388f893
Improve test validation for mk_transitivity
Copilot Feb 16, 2026
709d1b0
remove brittle pydoc example
NikolajBjorner Feb 16, 2026
2da8091
revert to last working flows
NikolajBjorner Feb 16, 2026
eed75bb
Initial plan
Copilot Feb 16, 2026
e9fcdd4
Add Go bindings support to ubuntu-cmake CI builds
Copilot Feb 16, 2026
25a83fc
Fix Go bindings compilation issues and add to CI
Copilot Feb 16, 2026
c61ee6b
Fix Go bindings and enable in CI
Copilot Feb 16, 2026
dd09b89
Fix trailing whitespace in Go source files
Copilot Feb 16, 2026
fa5f5c5
update version
NikolajBjorner Feb 16, 2026
95c17e5
Initial plan
Copilot Feb 16, 2026
436a2f8
Add Go bindings to API coherence checker workflow
Copilot Feb 16, 2026
beb7756
Initial plan
Copilot Feb 16, 2026
0ef12e3
Fix git sparse-checkout initialization in a3-python workflows
Copilot Feb 16, 2026
550b190
Initial plan
Copilot Feb 16, 2026
d1dd539
Add missing high-priority Go bindings to Solver
Copilot Feb 16, 2026
42c783a
Fix duplicate example in advanced_example.go and add silent markers f…
Copilot Feb 16, 2026
f734ce9
Address code review feedback: use os.CreateTemp and remove unused vars
Copilot Feb 16, 2026
b0702bf
Fix variable naming: tmpFile -> tempFile for Go conventions
Copilot Feb 16, 2026
0532efe
Initial plan
Copilot Feb 16, 2026
1536561
Fix Go bindings reference counting for Z3_ast_vector objects
Copilot Feb 16, 2026
d43c556
Initial plan
Copilot Feb 16, 2026
d56ae1a
Fix formatting of z3.go using gofmt
Copilot Feb 16, 2026
f2a41ca
Bump actions/cache from 4.3.0 to 5.0.3
dependabot[bot] Feb 16, 2026
7d58011
Bump github/gh-aw from 0.43.15 to 0.45.1
dependabot[bot] Feb 16, 2026
0cb36f9
Bump actions/checkout from 5.0.1 to 6.0.2
dependabot[bot] Feb 16, 2026
68e4a2a
Bump actions/download-artifact from 6.0.0 to 7.0.0
dependabot[bot] Feb 16, 2026
9e96ecb
Bump githubnext/gh-aw from 0.42.17 to 0.45.1
dependabot[bot] Feb 16, 2026
74ae287
Initial plan
Copilot Feb 17, 2026
3cad025
Simplify Go bindings: refactor GetLowerAsVector and GetUpperAsVector …
Copilot Feb 17, 2026
b8148b9
Initial plan
Copilot Feb 17, 2026
1163774
Initial plan: Fix a3-python.md workflow shell substitution issue
Copilot Feb 17, 2026
2f2c4d9
Remove problematic shell substitution from a3-python workflow
Copilot Feb 17, 2026
298803c
Fix shell substitution in a3-python-v2 workflow as well
Copilot Feb 17, 2026
cf60e7a
Initial plan
Copilot Feb 17, 2026
d5ba26e
Fix C4267 build warnings in ast.h by adding static_cast for size_t to…
Copilot Feb 17, 2026
534361d
fix #8563 - align indices for flat quantifiers with sks vector layout…
NikolajBjorner Feb 17, 2026
edb35e7
Initial plan
Copilot Feb 17, 2026
5ecbb9d
Add missing solver API functions to Go bindings
Copilot Feb 17, 2026
20f5967
Optimize TrailLevels and improve documentation
Copilot Feb 17, 2026
7da235a
Improve documentation clarity for new APIs
Copilot Feb 17, 2026
a04f255
Add safety comment and improve test documentation
Copilot Feb 17, 2026
d048eec
Delete examples/go/test_new_apis.go
NikolajBjorner Feb 17, 2026
3b89789
delete dead code
nunoplopes Feb 17, 2026
f065b84
remove irrelevant order-sign invariance tracking from levelwise
levnach Feb 17, 2026
7680f49
Initial plan
Copilot Feb 17, 2026
26c9adb
Upgrade agentic workflows to gh-aw v0.45.6
Copilot Feb 17, 2026
04b2fb3
Document upgrade changes and verify workflow compilation
Copilot Feb 17, 2026
7562de2
Remove checkout steps from A3 Python workflow
NikolajBjorner Feb 17, 2026
0f890da
Remove checkout steps from A3 Python workflow
NikolajBjorner Feb 17, 2026
cc74d55
recompile workflows
NikolajBjorner Feb 17, 2026
e261bac
new repository agnostic workflow
NikolajBjorner Feb 18, 2026
78a7b17
Update documentation generation to include Go
NikolajBjorner Feb 18, 2026
ac2cbdd
update a3-python to fix issues
NikolajBjorner Feb 18, 2026
05c301a
update go doc
NikolajBjorner Feb 18, 2026
5349fad
fixup docs.ytml
NikolajBjorner Feb 18, 2026
b5b7934
Initial plan
Copilot Feb 18, 2026
92d684e
Fix Priority 1 ASSERT_FAIL bugs - replace assertions with proper erro…
Copilot Feb 18, 2026
7e71ee9
Improve documentation for RatVal division by zero handling
Copilot Feb 18, 2026
bfdcfbe
Fix indentation in commented-out code section
Copilot Feb 18, 2026
f4b5dd8
Initial plan
Copilot Feb 18, 2026
200cb3d
Add --go flag to mk_api_doc.py calls and remove go directory overwrit…
Copilot Feb 18, 2026
3364bf2
remove deprecated workflows
NikolajBjorner Feb 18, 2026
04c1b04
Initial plan
Copilot Feb 18, 2026
8f4ecc8
Add missing API methods to Go and OCaml bindings
Copilot Feb 18, 2026
c22e20c
Add test for new Go API methods
Copilot Feb 18, 2026
29e759a
Delete examples/go/test_new_api_additions.go
NikolajBjorner Feb 18, 2026
316bc3d
Initial plan
Copilot Feb 18, 2026
2f33a34
Fix OCaml build error in solver_get_levels
Copilot Feb 18, 2026
fc792b6
update version
NikolajBjorner Feb 19, 2026
a1d43f5
fix build
NikolajBjorner Oct 18, 2025
c32b213
add finite sets to datatype recursion, delay initialize finite_set pl…
NikolajBjorner Oct 27, 2025
69b73c6
enable post setup parameter tweaking in theory solvers, update azure-…
NikolajBjorner Oct 28, 2025
07d8971
add sketch for incremental algorithm
NikolajBjorner Oct 30, 2025
7fe9b1f
Merge branch 'master' into finite-sets
NikolajBjorner Feb 19, 2026
24f36c2
Delete examples/SMT-LIB2/finite-sets/cycle.smt2
NikolajBjorner Feb 19, 2026
a32c9ef
remove examples
NikolajBjorner Feb 19, 2026
31a8592
Delete FINITE_SET_API.md
NikolajBjorner Feb 19, 2026
9f91380
next release notes
NikolajBjorner Feb 19, 2026
86dc556
add extra parameter
NikolajBjorner Feb 19, 2026
91a3068
disable a failure on a nullified poly in levelwise
levnach Feb 19, 2026
cd32dbe
Initial plan
Copilot Feb 19, 2026
ca8f379
Initial plan
Copilot Feb 19, 2026
d7aa454
Initial plan
Copilot Feb 19, 2026
9c8c9f5
Initial plan
Copilot Feb 19, 2026
0ad40a3
Remove unnecessary blank lines in mk_genfile_common.py and mk_api_doc.py
Copilot Feb 19, 2026
8a28bc2
Update nightly-validation.yml
NikolajBjorner Feb 19, 2026
866f352
Fix ambiguous svector constructor calls in theory_finite_set_lattice_…
Copilot Feb 19, 2026
2fa04f5
Merge pull request #8695 from Z3Prover/copilot/simplify-code-structure
NikolajBjorner Feb 19, 2026
c4acd2a
Fix macOS cross-compilation from ARM64 to x86_64 in mk_unix_dist.py a…
Copilot Feb 19, 2026
879dc93
Add tests for ackermannization module and Z3_algebraic_eval
Copilot Feb 19, 2026
ca1865c
Merge pull request #8696 from Z3Prover/copilot/fix-z3-import-error
NikolajBjorner Feb 19, 2026
44cd412
Merge pull request #8694 from Z3Prover/copilot/sub-pr-8686
NikolajBjorner Feb 19, 2026
23560ba
cleanup regarding levelwise
levnach Feb 19, 2026
5e5d9eb
Fix test_ackermannize_bv_model: skip crashing model converter test, k…
Copilot Feb 19, 2026
f414c79
Initial plan
Copilot Feb 19, 2026
c94eb5d
fixup API functions
NikolajBjorner Feb 19, 2026
426f839
Merge pull request #8691 from Z3Prover/no_fail
levnach Feb 19, 2026
ee03533
update examples to use arrays
NikolajBjorner Feb 19, 2026
5bd7d93
add parameter validation
NikolajBjorner Feb 19, 2026
093e227
Add ackermannize tests for mutation coverage
Copilot Feb 19, 2026
dbd7cd7
Fix off-by-one vulnerabilities: use range-based for on goals; cache l…
Copilot Feb 19, 2026
3698903
Merge pull request #8699 from Z3Prover/copilot/fix-missed-bugs-ff-by-one
NikolajBjorner Feb 19, 2026
bf73fdd
Merge pull request #8693 from Z3Prover/copilot/fix-test-coverage-gaps
NikolajBjorner Feb 19, 2026
38ce088
remove lattice component
NikolajBjorner Feb 19, 2026
385f913
try optimize handle_nullified_poly
levnach Feb 19, 2026
9c4e172
set the default of lws_spt_threshold to 4
levnach Feb 20, 2026
1521c43
Initial plan
Copilot Feb 20, 2026
e37624a
Update README.md banners: remove disabled workflows, fix WASM link, a…
Copilot Feb 20, 2026
3d8dd0d
update params
NikolajBjorner Feb 20, 2026
99e1ba3
update macos runner id
NikolajBjorner Feb 20, 2026
c56e033
Merge pull request #8700 from Z3Prover/copilot/update-readme-banners-…
NikolajBjorner Feb 20, 2026
30e4c9a
Fix badge links in README.md
NikolajBjorner Feb 20, 2026
8314aec
Merge pull request #8686 from Z3Prover/finite-sets
NikolajBjorner Feb 20, 2026
8f9c527
Merge branch 'master' into nl2lin
ValentinPromies Feb 20, 2026
6d3f3f2
fix
ValentinPromies Feb 20, 2026
95afda3
move linear cell construction to levelwise
ValentinPromies Feb 20, 2026
3a995bb
fix
ValentinPromies Feb 23, 2026
77d81de
fix
ValentinPromies Mar 6, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
5 changes: 4 additions & 1 deletion .gitattributes
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,7 @@

src/api/dotnet/Properties/AssemblyInfo.cs text eol=crlf

.github/workflows/*.lock.yml linguist-generated=true merge=ours
.github/workflows/*.lock.yml linguist-generated=true merge=ours

# Use bd merge for beads JSONL files
.beads/issues.jsonl merge=beads
123 changes: 123 additions & 0 deletions .github/CI_MIGRATION.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,123 @@
# Azure Pipelines to GitHub Actions Migration

## Overview

This document describes the migration from Azure Pipelines (`azure-pipelines.yml`) to GitHub Actions (`.github/workflows/ci.yml`).

## Migration Summary

All jobs from the Azure Pipelines configuration have been migrated to GitHub Actions with equivalent or improved functionality.

### Jobs Migrated

| Azure Pipelines Job | GitHub Actions Job | Status |
|---------------------|-------------------|--------|
| LinuxPythonDebug (MT) | linux-python-debug (MT) | ✅ Migrated |
| LinuxPythonDebug (ST) | linux-python-debug (ST) | ✅ Migrated |
| ManylinuxPythonBuildAmd64 | manylinux-python-amd64 | ✅ Migrated |
| ManyLinuxPythonBuildArm64 | manylinux-python-arm64 | ✅ Migrated |
| UbuntuOCaml | ubuntu-ocaml | ✅ Migrated |
| UbuntuOCamlStatic | ubuntu-ocaml-static | ✅ Migrated |
| UbuntuCMake (releaseClang) | ubuntu-cmake (releaseClang) | ✅ Migrated |
| UbuntuCMake (debugClang) | ubuntu-cmake (debugClang) | ✅ Migrated |
| UbuntuCMake (debugGcc) | ubuntu-cmake (debugGcc) | ✅ Migrated |
| UbuntuCMake (releaseSTGcc) | ubuntu-cmake (releaseSTGcc) | ✅ Migrated |
| MacOSPython | macos-python | ✅ Migrated |
| MacOSCMake | macos-cmake | ✅ Migrated |
| LinuxMSan | N/A | ⚠️ Was disabled (condition: eq(0,1)) |
| MacOSOCaml | N/A | ⚠️ Was disabled (condition: eq(0,1)) |

## Key Differences

### Syntax Changes

1. **Trigger Configuration**
- Azure: `jobs:` with implicit triggers
- GitHub: Explicit `on:` section with `push`, `pull_request`, and `workflow_dispatch`

2. **Job Names**
- Azure: `displayName` field
- GitHub: `name` field

3. **Steps**
- Azure: `script:` for shell commands
- GitHub: `run:` for shell commands

4. **Checkout**
- Azure: Implicit checkout
- GitHub: Explicit `uses: actions/checkout@v4`

5. **Python Setup**
- Azure: Implicit Python availability
- GitHub: Explicit `uses: actions/setup-python@v5`

6. **Variables**
- Azure: Top-level `variables:` section
- GitHub: Inline in job steps or matrix configuration

### Template Scripts

Azure Pipelines used external template files (e.g., `scripts/test-z3.yml`, `scripts/test-regressions.yml`). These have been inlined into the GitHub Actions workflow:

- `scripts/test-z3.yml`: Unit tests → Inlined as "Run unit tests" step
- `scripts/test-regressions.yml`: Regression tests → Inlined as "Run regressions" step
- `scripts/test-examples-cmake.yml`: CMake examples → Inlined as "Run examples" step
- `scripts/generate-doc.yml`: Documentation → Inlined as "Generate documentation" step

### Matrix Strategies

Both Azure Pipelines and GitHub Actions support matrix builds. The migration maintains the same matrix configurations:

- **linux-python-debug**: 2 variants (MT, ST)
- **ubuntu-cmake**: 4 variants (releaseClang, debugClang, debugGcc, releaseSTGcc)

### Container Jobs

Manylinux builds continue to use container images:
- `quay.io/pypa/manylinux_2_34_x86_64:latest` for AMD64
- `quay.io/pypa/manylinux2014_x86_64:latest` for ARM64 cross-compilation

### Disabled Jobs

Two jobs were disabled in Azure Pipelines (with `condition: eq(0,1)`) and have not been migrated:
- **LinuxMSan**: Memory sanitizer builds
- **MacOSOCaml**: macOS OCaml builds

These can be re-enabled in the future if needed by adding them to the workflow file.

## Benefits of GitHub Actions

1. **Unified Platform**: All CI/CD in one place (GitHub)
2. **Better Integration**: Native integration with GitHub features (checks, status, etc.)
3. **Actions Marketplace**: Access to pre-built actions
4. **Improved Caching**: Better artifact and cache management
5. **Cost**: Free for public repositories

## Testing

To test the new workflow:

1. Push a branch or create a pull request
2. The workflow will automatically trigger
3. Monitor progress in the "Actions" tab
4. Review job logs for any issues

## Deprecation Plan

1. ✅ Create new GitHub Actions workflow (`.github/workflows/ci.yml`)
2. 🔄 Test and validate the new workflow
3. ⏳ Run both pipelines in parallel for a transition period
4. ⏳ Once stable, deprecate `azure-pipelines.yml`

## Rollback Plan

If issues arise with the GitHub Actions workflow:
1. The original `azure-pipelines.yml` remains in the repository
2. Azure Pipelines can be re-enabled if needed
3. Both can run in parallel during the transition

## Additional Resources

- [GitHub Actions Documentation](https://docs.github.com/en/actions)
- [Migrating from Azure Pipelines to GitHub Actions](https://docs.github.com/en/actions/migrating-to-github-actions/migrating-from-azure-pipelines-to-github-actions)
- [GitHub Actions Syntax Reference](https://docs.github.com/en/actions/reference/workflow-syntax-for-github-actions)
132 changes: 132 additions & 0 deletions .github/CI_TESTING.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,132 @@
# Testing the CI Workflow

This document provides instructions for testing the new GitHub Actions CI workflow after migration from Azure Pipelines.

## Quick Test

To test the workflow:

1. **Push a branch or create a PR**: The workflow automatically triggers on all branches
2. **View workflow runs**: Go to the "Actions" tab in GitHub
3. **Monitor progress**: Click on a workflow run to see job details

## Manual Trigger

You can also manually trigger the workflow:

1. Go to the "Actions" tab
2. Select "CI" from the left sidebar
3. Click "Run workflow"
4. Choose your branch
5. Click "Run workflow"

## Local Validation

Before pushing, you can validate the YAML syntax locally:

```bash
# Using yamllint (install with: pip install yamllint)
yamllint .github/workflows/ci.yml

# Using Python PyYAML
python3 -c "import yaml; yaml.safe_load(open('.github/workflows/ci.yml'))"

# Using actionlint (install from https://github.com/rhysd/actionlint)
actionlint .github/workflows/ci.yml
```

## Job Matrix

The CI workflow includes these job categories:

### Linux Jobs
- **linux-python-debug**: Python-based build with make (MT and ST variants)
- **manylinux-python-amd64**: Python wheel build for manylinux AMD64
- **manylinux-python-arm64**: Python wheel build for manylinux ARM64 (cross-compile)
- **ubuntu-ocaml**: OCaml bindings build
- **ubuntu-ocaml-static**: OCaml static library build
- **ubuntu-cmake**: CMake builds with multiple compilers (4 variants)

### macOS Jobs
- **macos-python**: Python-based build with make
- **macos-cmake**: CMake build with Julia support

## Expected Runtime

Approximate job durations:
- Linux Python builds: 20-30 minutes
- Manylinux Python builds: 15-25 minutes
- OCaml builds: 25-35 minutes
- CMake builds: 25-35 minutes each variant
- macOS builds: 30-40 minutes

Total workflow time (all jobs in parallel): ~40-60 minutes

## Debugging Failed Jobs

If a job fails:

1. **Click on the failed job** to see the log
2. **Expand failed steps** to see detailed output
3. **Check for common issues**:
- Missing dependencies
- Test failures
- Build errors
- Timeout (increase timeout-minutes if needed)

4. **Re-run failed jobs**:
- Click "Re-run failed jobs" button
- Or "Re-run all jobs" to test everything

## Comparing with Azure Pipelines

To compare results:

1. Check the last successful Azure Pipelines run
2. Compare job names and steps with the GitHub Actions workflow
3. Verify all tests pass with similar coverage

## Differences from Azure Pipelines

1. **Checkout**: Explicit `actions/checkout@v4` step (was implicit)
2. **Python Setup**: Explicit `actions/setup-python@v5` step (was implicit)
3. **Template Files**: Inlined instead of external templates
4. **Artifacts**: Uses `actions/upload-artifact` (if needed in future)
5. **Caching**: Can add `actions/cache` for dependencies (optional optimization)

## Adding Jobs or Modifying

To add or modify jobs:

1. Edit `.github/workflows/ci.yml`
2. Follow the existing job structure
3. Use matrix strategy for variants
4. Add appropriate timeouts (default: 90 minutes)
5. Test your changes on a branch first

## Optimization Opportunities

Future optimizations to consider:

1. **Caching**: Add dependency caching (npm, pip, opam, etc.)
2. **Artifacts**: Share build artifacts between jobs
3. **Concurrency**: Add concurrency groups to cancel outdated runs
4. **Selective Execution**: Skip jobs based on changed files
5. **Self-hosted Runners**: For faster builds (if available)

## Rollback Plan

If the GitHub Actions workflow has issues:

1. The original `azure-pipelines.yml` is still in the repository
2. Azure Pipelines can be re-enabled if needed
3. Both systems can run in parallel during transition

## Support

For issues or questions:

1. Check GitHub Actions documentation: https://docs.github.com/en/actions
2. Review the migration document: `.github/workflows/CI_MIGRATION.md`
3. Check existing GitHub Actions workflows in `.github/workflows/`
4. Open an issue in the repository
Loading
Loading