| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
This PR refactors the contrib script to download SymFPU to a cmake external project.
|
|
This PR refactors our first, and arguably most fragile, dependency.
Right now all dependencies need to be manually installed (by calling the appropriate contrib/get-X script). For optional dependencies, we additionally need to enable them when calling the configure script (or via ccmake).
This PR is the first step in refactoring all dependencies to be automatically build (if required) as an external project.
Note that this not only eliminates the need to call contrib scripts, but also simplifies cross compilation: as all dependencies are now built within the build folders, every build folder has its own copy which may use different toolchains.
|
|
|
|
This commit refactors the run_regression.py script and adds options for enabling/disabling checking of proofs and unsat cores. Both options are enabled by default and disabled for each corresponding CI build.
|
|
This will help reduce the CI times and ccache sizes.
|
|
|
|
|
|
|
|
This fixes some issues that break the nightly ASAN builds with clang.
|
|
./configure.sh will now fail if Python3 is not installed on the system. Since Python2 is now deprecated the user has to explicitly enable it via --python2. This commit also removes the --python3 configure flag.
|
|
This sets up the infrastructure for migrating unit tests from CxxTest to
Google Test. It further migrates api/datatype_api_black to the new
infrastructure.
|
|
|
|
If building with python bindings, check the pytest is installed, and adds a command to run pytest after the existing make check tests. If built without python bindings, it just uses a null command. Note: the current semantics are such that the pytest tests will not run if the ctest run fails (unless you pass the correct flag to make to continue --ignore-errors I believe). I can look into changing this semantics if that would be preferred.
|
|
|
|
|
|
GH introduced a new workflow event pull_request_target that now makes it
possible to cancel builds on the base repository.
|
|
Commit e969318 introduced the ICP-based
solver for nonlinear arithmetic. That code, however, depends on LibPoly.
When configuring CVC4 without LibPoly, the code doesn't compile because
the class ICPSolver is missing. This commit adds a dummy version if
ICPSolver to remedy the issue.
|
|
Cython has been causing issues recently, see e.g.
https://github.com/CVC4/CVC4/pull/4982/checks?check_run_id=1052433862.
It looks like the issue is that globally installed packages can't be
found by Python (maybe the global site-package directories changed/are
not included in the search paths anymore?). This commit changes the
installation of Cython to install it locally to the user instead of
globally. It also adds `bin` in the user base directory to `PATH` s.t.
CMake is able to find the `cython` binary.
|
|
|
|
Since
https://github.com/CVC4/LFSC/commit/1d1c55fa17b08e2bc8cb686b9d07ec63bf0dd4a2
LFSC requires Flex, so we need to install the corresponding packages in
our CI environment. This commit also removes SWIG from the list of
packages to install since we do not use it anymore.
|
|
The previously introduced action to cancel running builds is not able to
cancel builds on other branches, only on the same branch. As a consequence,
when pushing to a branch for which a PR has been submitted, builds on the
main repository are not cancelled.
This removes the cancel build. If we want behavior similar to how it was
on Travis, we need a workaround / more sophisticated solution since GH
Actions doesn't really allow / support this (due to permission issues).
|
|
dependencies (#4809)
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
|
|
|
|
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
|
