Skip to content

Commit 2f5e62a

Browse files
authored
Merge pull request #56 from tweag/qa/0.3
release version 0.3
2 parents 366d2f4 + b8955c1 commit 2f5e62a

File tree

9 files changed

+119
-58
lines changed

9 files changed

+119
-58
lines changed

CHANGELOG.md

Lines changed: 30 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,40 @@
1-
see also the changelogs of `smtlib-backends-tests`, `smtlib-backends-process` and
2-
`smtlib-backends-z3`
1+
# Changelog
32

4-
# v0.3-alpha
5-
- **(breaking change)** add a datatype `Backends.QueuingFlag` to set the queuing mode
3+
All notable changes to the smtlib-backends library will be documented in this
4+
file.
5+
6+
The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
7+
and this project adheres to [PVP versioning](https://pvp.haskell.org/).
8+
9+
The same stands for the changelogs of
10+
[smtlib-backends-tests](smtlib-backends-tests/CHANGELOG.md),
11+
[smtlib-backends-process](smtlib-backends-process/CHANGELOG.md) and
12+
[smtlib-backends-z3](smtlib-backends-z3/CHANGELOG.md), except the version
13+
numbers simply follow that of `smtlib-backends`.
14+
15+
## v0.3 _(2023-02-03)_
16+
17+
### Added
18+
- **(breaking change)** add a datatype `Backends.QueuingFlag` to set the queuing
19+
mode
620
- the `initSolver` function now takes this datatype as argument instead of a
721
boolean
22+
- **(breaking change)** add a `send_` method to the `Backends.Backend` datatype
23+
for sending commands with no output
24+
- add a `Backends.flushQueue` function for forcing the content of the queue to
25+
be evaluated
26+
27+
### Changed
828
- **(breaking change)** make the queuing functions thread-unsafe but faster
9-
- add a `send_` method to the `Backends.Backend` datatype for sending commands with no output
10-
- add a `Backends.flushQueue` function for forcing the content of the queue to be
11-
evaluated
1229

13-
# v0.2
30+
## v0.2 _(2022-12-16)_
31+
32+
### Changed
1433
- split the `Process` module into its own library
1534
- rename `SMTLIB.Backends`'s `ackCommand` to `command_`
35+
- improve read-me
36+
37+
### Removed
1638
- remove logging abilities
1739
- the user can always surround `command` or `command_` with their own logging
1840
functions
19-
- improve read-me

README.md

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -31,34 +31,36 @@ It requires the libraries `smtlib-backends` and `smtlib-backends-process`.
3131

3232
More examples of how to use the different backends are included in their
3333
respective test-suites:
34-
- [examples for the `Process` backend](smtlib-backends-process/tests/Examples.hs)
34+
- [examples for the `Process`
35+
backend](smtlib-backends-process/tests/Examples.hs)
3536
- [examples for the `Z3` backend](smtlib-backends-z3/tests/Examples.hs)
3637

3738
## Building and testing
3839

3940
This repository provides a reproducible build environment through a [Nix
4041
flake](https://www.tweag.io/blog/2020-05-25-flakes/).
4142

42-
Another option is to manually install Z3 to use the process backend, and the
43-
Z3 C library to use the Z3 backend. Then you can build and test the libraries
44-
using `cabal build` and `cabal test`.
43+
Another option is to manually install Z3 to use the process backend, and the Z3
44+
C library to use the Z3 backend. Then you can build and test the libraries using
45+
`cabal build` and `cabal test`.
4546

4647
## Implementing backends
4748

4849
Currently, backends only need to provide a function to submit queries, as
4950
documented in [SMTLIB.Backends.Backend](src/SMTLIB/Backends.hs). See
50-
[SMTLIB.Backends.Process.toBackend](smtlib-backends-process/src/SMTLIB/Backends/Process.hs) or
51-
[SMTLIB.Backends.Z3.toBackend](smtlib-backends-z3/src/SMTLIB/Backends/Z3.hs) for examples.
51+
[SMTLIB.Backends.Process.toBackend](smtlib-backends-process/src/SMTLIB/Backends/Process.hs)
52+
or [SMTLIB.Backends.Z3.toBackend](smtlib-backends-z3/src/SMTLIB/Backends/Z3.hs)
53+
for examples.
5254

5355
## Motivation
5456

55-
This library was created because there are a lot of Haskell projects using SMT solvers
56-
through SMT-LIB, but most of them only use solvers through external processes
57-
and implement the interaction with the solver themselves. But running solvers
58-
as external processes can be quite slow, hence this library aims to provide
59-
other, more efficient ways to do so. We believe having one well-optimized and
60-
safe library is more efficient than having the same code be spread out between
61-
different projects.
57+
This library was created because there are a lot of Haskell projects using SMT
58+
solvers through SMT-LIB, but most of them only use solvers through external
59+
processes and implement the interaction with the solver themselves. But running
60+
solvers as external processes can be quite slow, hence this library aims to
61+
provide other, more efficient ways to do so. We believe having one
62+
well-optimized and safe library is more efficient than having the same code be
63+
spread out between different projects.
6264

6365
## Contributing
6466

smtlib-backends-process/CHANGELOG.md

Lines changed: 28 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,32 +1,45 @@
1-
# v0.3-alpha
2-
- make test-suite compatible with `smtlib-backends-0.3`
1+
# Changelog
2+
3+
All notable changes to the smtlib-backends-process library will be documented in
4+
this file.
5+
6+
## v0.3 _(2023-02-03)_
7+
8+
### Added
39
- add tests for documenting edge cases of the backends
410
- check that we can pile up procedures for exiting a process
511
- what happens when sending an empty command
612
- what happens when sending a command not producing any output
7-
- add `Process.defaultConfig`, synonym for `def`
8-
- improve error messages inside `Process.toBackend`
13+
- add `Process.defaultConfig`
14+
- add `std_err` field in `Config`: the user may now specifiy how to create the
15+
handle for the error channel
16+
17+
### Changed
18+
- make the test-suite compatible with `smtlib-backends-0.3`
919
- **(breaking change)** use `process` instead of `typed-process` to manage the underlying process
1020
- change the definition of the `Process.Handle` datatype accordingly
1121
- remove `Process.wait`
1222
- there is now a single example in the test-suite showing how to
1323
manage the underlying process and its I/O channels
24+
- improve error messages inside `Process.toBackend`
25+
26+
### Removed
27+
- removed `Process.wait`
1428
- **(breaking change)** removed logging capabilities, this is now on the user to
15-
implement
29+
implement (see also the `underlyingProcess` example)
1630
- remove `Config`'s `reportError` field
1731
- remove `Handle`'s `errorReader` field
1832
- **(breaking change)** removed `Data.Default` instance of `Config`
1933

20-
# v0.2
21-
split `smtlib-backends`'s `Process` module into its own library
22-
## `Config` datatype
23-
- move the logger function into it
24-
- make it an instance of the `Default` typeclass
25-
## logging
26-
- move the logger function into the `Config` datatype
34+
## v0.2 _(2022-12-16)_
35+
36+
### Added
37+
- made `Config` an instance of the `Default` typeclass
38+
- add usage examples in the test-suite
39+
40+
### Changed
41+
- split `smtlib-backends`'s `Process` module into its own library
42+
- move the logger function inside the `Config` datatype
2743
- don't prefix error messages with `[stderr]`
28-
## test-suite
29-
- add usage examples
3044
- make compatible with `smtlib-backends-0.2`
31-
## miscellaneous
3245
- improve documentation

smtlib-backends-process/smtlib-backends-process.cabal

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@ name: smtlib-backends-process
22
version: 0.3
33
synopsis: An SMT-LIB backend running solvers as external processes.
44
description:
5-
This library implements an SMT-LIB backend (in the sense of the smtlib-backends
6-
package) using by running solvers as external processes.
5+
This library implements an SMT-LIB backend (in the sense of the
6+
smtlib-backends package) which runs solvers as external processes.
77

88
license: MIT
99
license-file: LICENSE
@@ -22,7 +22,7 @@ source-repository head
2222
source-repository this
2323
type: git
2424
location: https://github.com/tweag/smtlib-backends
25-
tag: 0.2
25+
tag: 0.3
2626
subdir: smtlib-backends-process
2727

2828
library

smtlib-backends-tests/CHANGELOG.md

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,17 @@
1-
# v0.3-alpha
1+
# Changelog
2+
3+
All notable changes to the smtlib-backends-tests library will be documented in
4+
this file.
5+
6+
## v0.3 _(2023-02-03)_
7+
8+
### Changed
29
- make test-suite compatible with `smtlib-backends-0.3`
310

4-
# v0.2
5-
- remove `(exit)` commands at the end of sources
11+
## v0.2 _(2022-12-16)_
12+
13+
### Changed
614
- make library compatible with `smtlib-backends-0.2`
15+
16+
### Removed
17+
- remove `(exit)` commands at the end of sources

smtlib-backends-tests/smtlib-backends-tests.cabal

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ source-repository head
2222
source-repository this
2323
type: git
2424
location: https://github.com/tweag/smtlib-backends
25-
tag: 0.2
25+
tag: 0.3
2626
subdir: smtlib-backends-tests
2727

2828
library

smtlib-backends-z3/CHANGELOG.md

Lines changed: 23 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,30 @@
1-
# v0.3-alpha
2-
- make test-suite compatible with `smtlib-backends-0.3`
3-
- **(breaking change)** the `Z3.new` and `Z3.with` functions now take a `Z3.Config`
4-
object as argument, which one may use to set some solver options at initialization
5-
time
6-
- add corresponding examples in the test-suite
7-
- add `Z3.defaultConfig`, synonym for `def`
1+
# Changelog
2+
3+
All notable changes to the smtlib-backends-z3 library will be documented in this
4+
file.
5+
6+
## v0.3 _(2023-02-03)_
7+
8+
### Added
9+
- add `Z3.defaultConfig`
810
- add tests for documenting edge cases of the backends
911
- what happens when sending an empty command
1012
- what happens when sending a command not producing any output
1113
- **(breaking change)** removed `Data.Default` instance of `Config`
14+
15+
### Changed
16+
- make test-suite compatible with `smtlib-backends-0.3`
17+
- **(breaking change)** the `Z3.new` and `Z3.with` functions now take a
18+
`Z3.Config` object as argument, which one may use to set some solver options
19+
at initialization time
20+
- add corresponding examples in the test-suite
1221
- dropped dependency on `inline-c`
22+
- removed `Data.Default` instance for `Config`
1323

14-
# v0.2
15-
- make test-suite compatible with `smtlib-backends-0.2`
24+
## v0.2 _(2022-12-16)_
25+
26+
### Added
1627
- add usage examples in the test-suite
28+
29+
### Changed
30+
- make test-suite compatible with `smtlib-backends-0.2`

smtlib-backends-z3/smtlib-backends-z3.cabal

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ source-repository head
2424
source-repository this
2525
type: git
2626
location: https://github.com/tweag/smtlib-backends
27-
tag: 0.2
27+
tag: 0.3
2828
subdir: smtlib-backends-z3
2929

3030
library

smtlib-backends.cabal

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,9 @@ synopsis:
55

66
description:
77
This library provides an extensible interface for interacting with SMT solvers
8-
using SMT-LIB. The smtlib-backends-process provides a backend that runs solvers
9-
as external processes, and the smtlib-backends-z3 package provides a backend that
10-
uses inlined calls to Z3's C API.
8+
using SMT-LIB. The smtlib-backends-process package provides a backend that
9+
runs solvers as external processes, and the smtlib-backends-z3 package
10+
provides a backend that uses inlined calls to Z3's C API.
1111

1212
license: MIT
1313
license-file: LICENSE
@@ -25,7 +25,7 @@ source-repository head
2525
source-repository this
2626
type: git
2727
location: https://github.com/tweag/smtlib-backends
28-
tag: 0.2
28+
tag: 0.3
2929

3030
library
3131
hs-source-dirs: src

0 commit comments

Comments
 (0)