Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

V6.1.0 rc #3744

Merged
merged 13 commits into from
Nov 8, 2023
60 changes: 60 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,66 @@
copyright: Copyright (c) K Team. All Rights Reserved.
---

K Framework 6.1.0
=================

Features
--------
- Added support for MacOS 13 Ventura and Debian 12 Bookworm. We dropped support for
radumereuta marked this conversation as resolved.
Show resolved Hide resolved
Ubuntu 20 Focal. You can now build K from sources on Apple Silicon. See README
radumereuta marked this conversation as resolved.
Show resolved Hide resolved
for more details.

- Updated dependency to Java version 17 or higher.

- Added the Haskell Backend Booster as a dependency to K. This can improve performance
when running large proofs. It combines the llvm-backend for concrete execution and
radumereuta marked this conversation as resolved.
Show resolved Hide resolved
relies on the haskell-backend to simplify terms when there is a split in the proof.
radumereuta marked this conversation as resolved.
Show resolved Hide resolved

- Optimized the kompiler by removing unit applications for collections.

- Minimize JSON output by dropping unused attributes

- Added `--smt-timeout` flag to `krun` and `kprove`.

- Changed the Maven repository to Cloudrepo for more stability and flexibility when
building K from sources.

- Improved attribute error messages by creating a whitelist dependent on the context.
This check is now mandatory.

- Rule label cannot contain ` or whitespace
radumereuta marked this conversation as resolved.
Show resolved Hide resolved

- Improved the help messages by adding a description of the expected parameter.

- Documentation: Started work on Section 2 of the tutorial. Added a description for
`kserver`.

- Added `--debugger-command` flag to krun.

- Added two options `--debug-tokens` and `--debug-parse` to help with debugging
parsing errors. The first option will print a Markdown table with all the matched
tokens by the scanner. The second one will give more details about the partial parse
tree constructed before an error was encountered.

Misc/Bug Fixes
--------------
- Fixed a bug where the llvm backend would segfault because of badly initialized
radumereuta marked this conversation as resolved.
Show resolved Hide resolved
fresh variables in the configuration.

- Improved performance for JSON creation.

- Remove old unused attributes.

- Fix output sorting for KPrint. This will create a more stable pretty printed output.

- Fix configuration pretty printing where `<generatedCounter>` would appear instead
of a closing cell.

- Moved a README file from the `builtin` directory that could collide with users' files.

A more detailed list of changes can be found here:
https://github.com/runtimeverification/k/issues/3706

K Framework 6.0.0
=================

Expand Down
2 changes: 1 addition & 1 deletion install-k
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
#!/bin/sh -e

K_VERSION=6.0.0
K_VERSION=6.1.0

if [ `id -u` -ne 0 ]; then
echo "$0: error: This script must be run as root."
Expand Down
2 changes: 1 addition & 1 deletion package/arch/PKGBUILD
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Maintainer: Dwight Guth <[email protected]>
pkgname=kframework-git
pkgver=6.0.0
pkgver=6.1.0
pkgrel=1
epoch=
pkgdesc="K framework toolchain. Includes K Framework compiler for K language definitions, and K interpreter and prover for programs written in languages defined in K."
Expand Down
2 changes: 1 addition & 1 deletion package/debian/changelog
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
kframework (6.0.0) unstable; urgency=medium
kframework (6.1.0) unstable; urgency=medium

* Initial Release.

Expand Down
2 changes: 1 addition & 1 deletion package/version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
6.0.0
6.1.0
Loading