| Age | Commit message (Collapse) | Author |
|---|
|
This PR enables CI for java tests by adding --java-bindings to ci.yml.
It also replaces the unreliable finalize method and instead uses AutoCloseable and explicit close method to clean up dynamic memory allocated by java native interface.
The PR fixes compile errors for SolverTest.java and runtime errors for Solver.defineFun.
|
|
This PR fixes multiple issues with uploading docs for releases: the regular upload moved the generated docs, so the release upload would not find the docs; the check whether we have a release was incorrect; we probably want $NAME instead of docs-$NAME here.
|
|
This PR combines the two configure flags --static and --static-binary into a single --static. Consequently, the two corresponding cmake variables are combined as well. The two variables have been implying each other for some time now and were only used to build not-completely-static binaries for MacOS, which is now done automatically anyway.
|
|
This PR changes our strategy to deal with shared vs. static builds in CI jobs.
All jobs now build cvc5 both shared and static by default. The builds happen in different build directories (build-shared and build-static), and we configure ccache such that these two build directories share a common cache.
|
|
This PR adds documentation on how users can use -o. After some offline discussion, we decided it makes sense to generate them automatically in mkoptions.py and also include example outputs.
|
|
This automatically uploads the generated docs to a new repository docs-releases (which should eventually become docs). In contrast to docs-ci, we only store docs for releases there.
|
|
This makes the regression script more modular by refactoring all the
different checks into separate classes, which makes it easier to add
additional tests and to run only a subset of the tests.
|
|
This is a follow-up to #7420. This time, I tested the modified code with every combination of values...
|
|
This fixes an issue introduced with #7352: jobs fail immediately if any command has a non-zero exit code. The way we obtained the exit code of the `diff` command was incompatible with this policy, which is why we currently never upload any docs to `docs-ci`.
|
|
This PR improves our docs-ci mechanism to properly upload documentation for tags.
|
|
This PR generally improves the new CI job to test different cmake versions. It extends the tested versions back to 3.8 and also sets the minimum required version (cmake_minimum_required) to the version that is tested. This allows to check compatibility with changing cmake policies.
It also modifies the run-tests action to get the regression options from explicit inputs instead of the build matrix. As the cmake job had no build matrix, it used to build regress3-4 as well.
|
|
|
|
This refactors the CI setup by moving parts of the CI workflow into new composite actions. This allows to reuse this parts in a new workflow that tests against many different cmake versions. It is mostly useful after modifying our cmake setup to check compatibility with older cmake versions.
The workflow is not triggered automatically, but can be started manually.
|
|
This fixes the diff mechanism to detect whether the current PR changes the documentation. It ignores zip files now, i.e. the javadoc search index files.
|
|
This adds another step to our CI pipeline that uploads the binary build by some of the jobs to a release.
|
|
This PR modifies our CI builds to have two static production builds. These binaries will be used as release artifacts later.
|
|
Currently, we configure one of our builds to include unit tests but then
do not compile and run them. This commit adds a step to compile and run
the unit/API tests.
|
|
`macos-latest` is currently using macOS 10.15, so this updates the CI to use `mac-11` (Big Sur).
|
|
This PR adds api::Solver::getOptionInfo() that returns information about a single option, including its name, aliases, current and default value and its domain.
|
|
The docs-cleanup job squashes all commits from the docs-ci repository that are older than one month. The current solution to retrieve the newest commit older than this one month erroneously relied on the commit date. As the script cherry-picks all newer commits, it should rather use the author date, though. Unfortunately, rev-list does not support filtering by author date, hence we use awk now...
|
|
Fixes #7001. Commit c8bc488 introduced the use
of list(PREPEND ...) which was only introduced in version 3.15. We require
CMake 3.9 or later and this commit makes our build system compatible with older
CMake versions again. It also changes our CI to have two builds with Ubuntu
18.04 and two builds with Ubuntu 20.04 to better cover different versions of
build tools (including CMake 3.10).
|
|
|
|
This commit fixes a subtle issue with pruning the old docs from docs-ci. We remove docs that are older than one week. However, we used the commit date instead of the authored date. Since we actually squash the old commits (that are older than four weeks) regularly, the commit date is always newer.
|
|
macOS virtual machines have three available cores but we were only using two of them for our CI. This commit changes the CI to retrieve the number of available cores and then to use that to number to build and test cvc5.
|
|
This PR makes squashing olds commits in the docs-cleanup CI job more robust: it makes sure that the squash commit has a proper commit date and that we gracefully handle if there is nothing to squash.
|
|
Our Clang builds started to fail to link when the environment changed. This commit changes our CI to only use cached dependencies if the build environment has not changed.
|
|
This PR abandons the attempt to do the cleanup in a single rebase command, and instead squashes the old commits manually. The current solution does not handle conflicts properly. The new approach (which seems to be more robust) proceeds as follows (to squash $first..$last):
- checkout $last
- soft reset to $first (checkout $first, but keep changes in working copy)
- commit to squashed commit
- cherry-pick $last..HEAD from main branch
|
|
Fixes an oversight from #6601.
|
|
This PR reduces the disk size of the docs generated by make sphinx-gh.
Apart from reformatting the cmake source, we now not only remove the _sources folder, but also .doctrees (essentially the sphinx cache) and _static/fonts/ (the fonts that are actually used live in _static/css/fonts).
In combination, this now reduces the disk size from about 20MB (sphinx) to less than 6MB (sphinx-gh).
Furthermore this PR only uploads the generated documentation if it differs from whatever we currently have for master.
This is relevant to make the docs-ci repository smaller (which already has more than 5GB...)
|
|
This PR removes copied CMake files for the pycvc5 Cython target, and instead adds a dependency on scikit-build (where those CMake files originated anyway). This keeps us up to date with fixes. Furthermore, the PR switches from distutils to the more modern setuptools. This does add another dependency but it's a fairly reasonable one. setuptools is not part of the base Python distribution, but my understanding is that it is now the de facto standard, and most package managers install it automatically with Python. The main motivation for switching is in preparation for building wheels.
This PR is a piece of this old one (#5657) which I am closing and splitting up.
|
|
We currently have issues with clang 11 failing for white unit tests.
This disables unit tests for clang builds.
|
|
The new upload-docs CI job is currently run unconditionally after the CI job finishes. It can only work, though, if the CI job worked and stored an artifact. The PR update job is run for all commits on master, though it only has the necessary token when running on the main repository.
This PR restricts both jobs to cases where they work.
|
|
This PR (finally, I hope) uses a proper setup for uploading the documentation. One of the CI jobs generates the documentation and stores it in an artifact. Another workflow is triggered (via workflow_run) and then uploads this artifact. Only this setup seems to properly work for PR builds.
|
|
The new documentation workflow requires building CVC5 again in a separate workflow, which takes quite some time.
This PR integrates building the documentation with the regular CI workflow.
|
|
|
|
For PRs, the automatically generated documentation is stored under the current master commit hash instead of the hash of the latest commit on the PR. This PR fixes this issue by exporting the commit hash (much like the name of the PR or branch).
|
|
This PR adds --auto-download for the CI job that builds the documentation. Also makes sure that the documentation workflow never fails.
|
|
This PR adds CI jobs to automatically build documentation for branches on the main repository and for pull request.
The first job builds the documentation for every push and pr and stores the generated documentation in cvc5.github.io/docs-ci. All versions are stored and for every branch and PR a symbolic link to the most recent version is maintained.
Note that the PR jobs are run by the pull_request_target trigger that allows access to repository secrets, but runs in the context of the target branch and we thus need to (carefully!) pull in the relevant changes manually.
The second job runs once a week and prunes the docs-ci repository: all directories that have not been touched for a month are removed, and all commits older than a month are squashed into a single commit. This retains the full history for the last month, but effectively removes everything older than that.
|
|
This automatically applies @martin-cs's working patch from 2020-11-14.
It fixes several issues, all covered open issues are added as
regression tests.
Fixes #3582.
Fixes #5511.
Fixes #6164.
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
This PR changes a few things in how dependencies are handled during configuration:
- --x-dir are removed for most dependencies, use the generic --dep-path instead
- the cmake ENABLE_AUTO_DOWNLOAD determines whether we attempt to download missing dependencies ourselves
- external projects check this option and send an error if it is OFF
- some optional dependencies are enabled by default (CaDiCaL, Poly, SymFPU)
This will essentially fail every call to ./configure.sh until the user specifies --auto-download.
|
|
|
|
The build is currently failing because it tries to download an older
version of the ccache package. This commit makes sure that Homebrew is
up-to-date before trying to install packages.
|
|
The CI action we use to update PRs that are ready to merge has been updated and now only considers the last review of every reviewer. It now allows to automatically update (and then merge) PRs where a reviewer first requested changes, and then accepted the PR. See adRise/update-pr-branch#11 for more details.
This PR bumps the version to the most recent one.
|
|
|
|
This PR adds caching of the new dependencies folder build/deps/ for the CI jobs and renames the old deps folder to "auxiliary told".
Note that we need to cache the entirety of build/deps/ (instead of just the install folder for the old one), otherwise cmake will try to rebuild them. Some of the external projects remove unnecessary files in their build to reduce their footprint in the cache.
|
|
|
|
|
|
Refactors GMP and libpoly to also use external projects and be available within cmake as proper targets.
|
|
This PR refactors how we obtain, build and use the external SAT solvers used by CVC4: CaDiCaL, CryptoMiniSat and Kissat.
All three contrib scripts are removed and instead an external project is integrated into the cmake find scripts.
|
