Skip to content

Commit

Permalink
V6.1.0 rc (#3744)
Browse files Browse the repository at this point in the history
Mostly incremental changes.

Closes: #3706

Merge only if the release works.

---------

Co-authored-by: Bruce Collie <[email protected]>
  • Loading branch information
radumereuta and Baltoli authored Nov 8, 2023
1 parent 69ec6c3 commit e9ed600
Show file tree
Hide file tree
Showing 5 changed files with 63 additions and 4 deletions.
59 changes: 59 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,65 @@
copyright: Copyright (c) K Team. All Rights Reserved.
---

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

Features
--------
- Added support for MacOS 13 Ventura. We dropped support for Ubuntu 20.04 Focal.
K can now be built from source on Apple Silicon. See README 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 uses the LLVM Backend for concrete execution and
relies on the Haskell Backend to simplify terms when there is a split in the proof.

- 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 can no longer contain backticks (`) or whitespace.

- 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
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

0 comments on commit e9ed600

Please sign in to comment.