Build, Releases, Test automation #5078

NikolajBjorner · 2021-03-04T16:44:17Z

NikolajBjorner
Mar 4, 2021
Maintainer

Supporting and extending Z3 comes with a substantial amount of infrastructure work. I am listing a number of categories below.
Some of these topics could be suitable as an isolated side project as part of learning tools and processes that are used.
You can also comment below or contact me directly about getting involved.

General work items

Address github issues labeled “API / compilation”
Update regression tests with bug repros from last 1-2 years
- The question was raised at some point whether to contribute regression tests. This is welcome. They still need to pass or be disabled on check-in. The .expected.out files need to be formatted so the diff tool accepts them.
- With now several fuzzers exercising their tools on Z3 there is great benefit to the increased coverage.
  what is missing is additional follow up by fuzzers in the form of:
  - deeper triaging to identify root causes and even create fixes in easy cases.
  - integration of regression tests, though this seems less urgent because the distributed model of fuzzers running their regressions on their own is a real logistical advantage in several respects.
Set up regression and test suite targeted for weakly supported (complex) theories:
- strings/regex
- transitive closure
Add build test verification to azure pipelines the current Azure pipelines don’t test the release packages such as generated Nuget, but builds unit tests within z3’s build environment
Set up the Azure pipelines for sustained usage. For example, ESRP signing of packages with symbols is done with some copy-paste in the script. This could likely be streamlined to avoid duplicated near-identical commands.
Revise Ocaml build and API for missing API functions, build for Ubuntu 20, Windows build process
Port Ocaml build to cmake. It is currently only possible from python build system which means we cannot deprecate the otherwise obsolete python build environment.
Port release scripts from python build environments to cmake builds
Port jupyter environments with Z3 tutorials from deprecated Azure host to vscode or github environment or whatever is the new modus operandi
Overhaul Z3 tutorial and documentation: rise4fun is main entry point, but this misses API usage which is currently covered by programmingz3.html and the doxygen documentation
Update doxygen to readthedocs
Integrate clang style enforcement

Requires access to corporate network

Manage ESRP signing: update certs, update Azure pipeline build scripts for uniform ESRP signing process through nightly and release scripts
Manage Azure subscription updates from classical to current
Set up self-contained REST service with Z3 to decouple from rise4fun environment,
Code signing for MacOS (as described in github issue). This can probably be addressed by using a corporate signed certificate from Azure pipelines

Requires deeper engagement

revise AxiomProfiler functionality entirely based on DRAT output and deprecate ad-hoc trace.
- The current axiom profiler draws on a very deep integration, tracing every inference by the decision procedures with a separate, stand-alone, code-path. This approach is not sustainable and should not be used as a starting point for future developments.
Maintain an independent and principled DRAT(T) checker (there is a built-in checker accessible from the command-shell of Z3).

aytey · 2021-03-16T14:01:31Z

aytey
Mar 16, 2021

Port Ocaml build to cmake. It is currently only possible from python build
system which means we cannot deprecate the otherwise obsolete python build
environment.

Port release scripts from python build environments to cmake builds

I'm exclusively a user of the cmake way of doing things and never run ./configure -- can you provide some more details on what's required to totally sunset the Python build system and make everything be a first-class cmake citizen?

3 replies

NikolajBjorner Mar 16, 2021
Maintainer Author

In a nutshell, all commands used by
https://github.com/Z3Prover/z3/blob/master/scripts/release.yml
https://github.com/Z3Prover/z3/blob/master/scripts/nightly.yaml
should be cmake enabled.
These scripts call into other scripts that create releases.
For example:
https://github.com/Z3Prover/z3/blob/master/scripts/mk_win_dist.py

I am not sure why Levent still uses the python build other than maybe a desire to have fewer dependencies.
Though, cmake seems well engrained in build processes nowadays and avoids some kluges seen in the python build system.

The totality is probably fairly substantial work especially how things have been subject to evolution and I am not sure what would be a small atomic piece that is suitable for side-fun.

aytey Mar 16, 2021

For example:
https://github.com/Z3Prover/z3/blob/master/scripts/mk_win_dist.py

I mean, it isn't exactly "pleasurable", but I don't think converting that particular one to CMake would be too onerous.

small atomic piece

Yeah, my biggest concern is that this could be "all or nothing".

What if a first step is to wrap the legacy Python in CMake (but with no behaviour changes)? That way, the CI jobs could drive the old build system, but via CMake; e.g., something like -DLEGACY_BUILD:BOOL=ON -DLEGACY_ARGS:STRING="--java"?

Then, we can replace parts of the Python with first-class CMake without doing it all in one go.

NikolajBjorner Mar 16, 2021
Maintainer Author

I believe it doesn't make sense to waste efforts on including legacy python into cmake.
The cmake system already does pretty much everything of relevance.

The python release files were created long before the cmake build and then never considered to be ported.
There are several small details like copying license files and where the nuget package resides, but the pipeline scripts (or for that matter cmake) might take ownership of this now that releases are managed from pipelines instead of PC-centric stand-alone scripts.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Build, Releases, Test automation #5078

Uh oh!

{{title}}

Uh oh!

Replies: 1 comment 3 replies

Uh oh!

{{title}}

Uh oh!

Uh oh!

{{title}}

Uh oh!

Uh oh!

{{title}}

Uh oh!

Uh oh!

{{title}}

Uh oh!

Select a reply

Uh oh!

Build, Releases, Test automation #5078

Uh oh!

NikolajBjorner Mar 4, 2021 Maintainer

General work items

Requires access to corporate network

Requires deeper engagement

Replies: 1 comment · 3 replies

Uh oh!

aytey Mar 16, 2021

Uh oh!

NikolajBjorner Mar 16, 2021 Maintainer Author

Uh oh!

aytey Mar 16, 2021

Uh oh!

NikolajBjorner Mar 16, 2021 Maintainer Author

NikolajBjorner
Mar 4, 2021
Maintainer

Replies: 1 comment 3 replies

aytey
Mar 16, 2021

NikolajBjorner Mar 16, 2021
Maintainer Author

NikolajBjorner Mar 16, 2021
Maintainer Author