2023 Goals

[radumereuta]

A few general directions that we would like to follow in developing K in the year 2023:

• IDE integration through the Language Server Protocol LSP for K #3070
• K REPL - step through the program and semantics and make K, in general, easier to use K semantic REPL #2925
  • IDE integration through Debug Adapter Protocol
• KSummarizer/proof navigation tools that would allow for faster and easier-to-understand proving workflows.

[ehildenb]

https://docs.google.com/document/d/1NQQGuXiBlRBQMVfIo8eGAAgl3WsUlmVRsx7fJGKOxiA/edit

[Baltoli]

2023 Merged PRs

I plan to take a look through this list and try to see if there are any major themes that emerge.

#3864 Adopt #3862: "Update Bencher CLI version"
#3860 hot fix
#3858 hot fix (#3857)
#3857 hot fix
#3855 Enable new TI in kprove
#3853 Clean up {...}<:S strict cast syntax
#3850 Remove #parseKORE
#3846 Add more outdated warnings
#3843 Correct typo in performance tests in CI
#3841 Adopt scalafmt for Scala code style
#3840 Remove EAsSet[E] and WAsSet[W] traits in Transformers.scala to address IntelliJ error
#3834 Various improvements to POSet
#3828 Move id field out of ProductionReference into TypeInferencer
#3825 Move nailgun to lib/kframework/bin
#3823 Add k-which-python binary in nix
#3821 Add proof hint generation flag
#3819 Fix llvm backend bins in the k derivation
#3816 Address IntelliJ warnings in Interface.scala
#3814 Add KItem subsorts to the disambiguation module when parsing programs
#3813 Clean up cast insertion in TypeInferenceVisitor
#3812 Claim infer cell2
#3807 Remove unused strict field from ParseInModule
#3806 Remove mavenix take 2
#3805 Revert "Remove mavenix build"
#3804 make Pattern implement Comparable and also have an Ordering instance
#3802 Remove mavenix build
#3798 Add total to #let-bindings where LHS is a variable
#3797 Fix version of Google Java Format used in CI
#3796 Fix version of mavenix
#3794 Hotfix for release workflow re. macOS / python
#3793 Maven plugin for using google-java-format
#3792 Update Bencher's version
#3790 Run mvn verify with appropriate number of cores
#3789 Avoid overlap of equations for Bool combinators simplifications
#3785 Apply more automatic Java refactoring
#3783 Bump LLVM version in packaging to 15
#3781 Fix homebrew repo authentication
#3779 Revert #3773
#3778 Update release.yml
#3776 Move homebrew mentions to new repository
#3775 update the version of a couple vulnerable dependencies
#3774 Update README to address missing dependency
#3773 Finally remove PKGBUILD
#3772 Fix release cachix action
#3771 Revert experimental Homebrew changes
#3770 Temporary restore of arch PKGBUILD
#3768 Clean up Homebrew after running commands
#3767 Fix for Homebrew bottle name on arm64
#3766 Install wget in release job
#3765 Drop Arch Linux and Debian packaging
#3764 Move mac release CI to hosted ARM runners
#3761 Update README instructions
#3760 Temporary hotfixes for release flakiness
#3759 Add cachix binary cache publish step to release
#3757 Adopt Google Java style
#3755 Apply "silent code cleanup" from IntelliJ
#3754 Pin nixpkgs to haskell-backend
#3750 Apply Java migration: pattern variables
#3749 Revert to nix-community/mavenix in nix build
#3748 Update nix install script
#3746 Apply Java 17 automatic migration: records
#3745 Apply Java 17 automatic migration: enhanced switch
#3744 V6.1.0 rc
#3743 Check for Java 17 when running K tools
#3742 Fix release by installing Calibre 6
#3741 Fix for macOS nix / kup breakage
#3736 Bump JDK requirement to 17
#3734 Slimmer nix runtime closure
#3733 Add lowerBounds and upperBounds methods to POSet
#3725 Drop mentions of Focal from packaging and install documentation
#3724 Rephrase sed invocation for macOS
#3722 Support for memset hook.
#3717 Move PL tutorial link out of main "learn K" section
#3714 Move dockerhub image to prebuilt z3
#3709 Boost is a runtime dependency
#3703 Bump calibre version in release
#3702 Use new Z3 image location
#3701 Move README from builtin
#3700 Add option to print better parse errors
#3697 Use macos-13 everywhere
#3696 Point to new release.nix upload action
#3694 Use prebuilt z3 images
#3691 Packaging: version path fix
#3687 Introduces --debugger-command flag to krun
#3686 Builing MacOS Package on MacOS 13
#3683 Packaging: Move version into lib/kframework
#3679 Finish all changes to the K frontend, LLVM backend, and Haskell backend relating to multi-ary \and/\or
#3678 update scala kore parser to use multi-ary and and or everywhere
#3676 change case classes and parser to support multi-ary \and/\or.
#3673 Implement new sort inference algorithm
#3670 Ordering instance for Sentences (2)
#3666 Ensure type inference checks rhsSort <: lhsSort for macro rules
#3665 remove build extension for aws s3 that is no longer used
#3664 Updating Maven and Testing it
#3662 Check if macros were expanded in ensures and requires
#3660 kast --debug-tokens
#3659 Add llvm-kompile-matching to K package
#3658 Setting $workspace variable in develop.yml
#3655 Fixing develop.yml workflow
#3654 Refactor GeneratedTopFormat
#3653 Fix output sorting for KPrint
#3652 Clean up flake inputs
#3650 Finished page title generation
#3649 Fix K Version on Debian
#3648 Adding arguments to kprove flags
#3644 Updating Guice to 4.0 and deleting temporary injections
#3642 Adding arguments to kast flags
#3641 Update the container's name for correcting installing dependencies.
#3639 docs: 📝 Added section 2 docs
#3638 Improving kompile's --help and --help-hidden messages using descriptors
#3637 Installing dependences to bencher execution on develop
#3636 Fix parsing left/right-assoc kore terms in kast
#3631 Add K-ST
#3628 Fix gdate dependence: Use date -r instead of gdate -d on macOS to get k version
#3627 Adding CI to release workflow to create a develop baseline performance on Bencher
#3626 Fix k script to print --version correctly in docker container
#3623 Update krun usage message to contain [options]
#3622 Revert "Ordering instance for Sentences"
#3618 Improving Lesson 1.3 by mentioning longest match while scanning tokens
#3617 Update Lesson 1.2 to point to the correct further lesson/link
#3615 Fix token constructor error
#3611 Add Bencher to track Benchmarks Performance Regression
#3609 Testing run nix-flake on self hosted linux machine
#3608 Allow some rule-only attributes on sentences that desugar into rules
#3603 Adding profiling tests
#3602 Make no junk right associative
#3600 Remove focal image usage
#3597 Internal left/right attributes for c++ unparser
#3596 Rule label cannot contain ` or whitespace
#3594 Fix kore-integration-tests dev shell
#3592 Remove structural attribute
#3590 Ordering instance for Sentences
#3589 Allowed attributes for sentence types
#3588 print no-junk with flat multi-or
#3586 add TextToKore.parseModule
#3584 Fix Java 19
#3581 Changing pull maven repository to cloudrepo
#3579 Check parameters on attributes
#3578 Remove some old unused attributes
#3576 Add --smt-timeout flag to kprove
#3575 Add --smt-timeout flag to krun
#3569 Upload failure tar file to review build issue
#3568 Minimize JSON output by dropping unused attributes
#3567 Hotfix/maven release push
#3562 Add doc for kserver
#3561 Checks on main/syntax modules during module exclusion
#3560 More performance regressions
#3558 Increasing Build timeouts for jammy / focal to match arch / bookworm
#3557 Fresh constants for configuration initializers
#3554 Revert "AddKoreAttribute as a Frontend Kompiler Pass"
#3549 Make K derivation extensible with llvm libraries
#3543 update jung dependency
#3541 Update release.yml
#3529 [ModuleToKore Refactoring] Creatign GenerateMapCeilAxioms compiler pass
#3525 move integer lemmas out of code excluded by maude
#3524 rename MISSING_HOOK_JAVA warning to MISSING_HOOK and make it not hidden
#3523 Compare Attributes on Transformers
#3522 AddKoreAttribute as a Frontend Kompiler Pass
#3516 Set Arch release timeout to be longer
#3514 Haskell backend dependency chain updates
#3513 Fix release JDK version
#3512 Fix release build
#3510 Sync hs-backend submodule up manually
#3507 JSON creation - use object factory
#3506 Upgrade debian version to 12 bookworm
#3503 .github/workflows/update-deps: sync up booster release tag too
#3499 Remove the option to opt out of the attribute whitelist
#3497 Correctly escape ASCII values in the range 0-31
#3495 add haskell attribute to SET-KORE-SYMBOLIC
#3492 delete mounting of host's user and group info
#3489 Ensure that non-ASCII characters are escaped when emitting to KORE
#3487 Update documentation and tutorials for group(_)
#3484 Ensure module attributes are checked against the whitelist
#3483 simplify passing of environment variables to docker file
#3482 Commit flake.lock
#3480 update nixpkgs to nixos-23.05
#3476 Bumping install-nix-action to v22 and setting mac runners to macOS 13
#3475 Introducing the hs-backend-booster to K Framework
#3469 Remove unit applications in modules
#3468 Update booster binary name to kore-rpc-booster
#3467 Update CheckKLabels to consider --concrete-rules
#3466 try a better fix for the issue of creating the maven settings
#3464 Add booster to the k derivation
#3462 attempt to fix crash in maven deployment
#3461 Rangemap
#3459 Add generatedCounter implicitly to claims
#3458 Fix EOF parsing error message crash
#3457 Use private runner for release to fix out of space problem
#3456 Deploy artifacts to CloudRepo
#3455 Make the attribute whitelist opt-out
#3454 Improve --version implementation on K script
#3452 Update all K tests to use group(_)
#3443 Update attribute whitelist
#3441 Emit user-defined groups as group()
#3438 Throw error message when finding duplicate attributes
#3437 Check that sorts are well-formed for left, right, and non-assoc productions
#3434 Fix error message when missing sort
#3432 Implementing support for pretty printing non-terminals name
#3431 Update projects description
#3430 Improving kore-print script
#3428 Add an integration shell for haskell-backend
#3425 Remove all uses of the defunct [transition] attribute
#3424 Revert "Remove dead code HaskellKRunOptions"
#3423 Try and fix K release
#3422 Remove ResolveHeatCoolAttribute -O2/-O3 behavior
#3420 Pretty print NonTerminal names in generated txt files
#3419 Remove dead code HaskellKRunOptions
#3417 Create a hidden category for advanced options
#3414 Replacing deprecated option flag at tutorial tests
#3412 Restrict Bytes token syntax
#3409 Update make clean to account for a few missed test artifacts
#3407 Introduces --execute-to-branch to krun when using LLVM Backend
#3405 V6.0.0 rc
#3401 Fixing Kore label munging confusion
#3400 Setting --directory as deprecated
#3397 Add back Maven packages changes
#3395 Update missing KLabel checks to stabilize error messages
#3391 Make new-format rules without antileft the default
#3390 Add attribute whitelist and group() attribute
#3387 make field in KoreBackend protected instead of private
#3382 Add temp-dir option
#3379 Fix bottle name again
#3378 Add test for no-antileft rules with no explicit SC
#3375 Fix GeneratedCounterCell location
#3374 Use remote bottle path instead of local
#3371 Add UniqueId to all sentences, including generated ones
#3369 Revert Maven deployment changes
#3366 Fix can't find mvn
#3364 Updating mint-llvm Makefile and test from Haskell to LLVM Backend
#3362 Working around for cp unable to resolve incontainer tilden expession
#3357 Update Matrix links for use in any client [external: #3353]
#3356 Add check for manual declaration of isSort
#3355 Update version of C tools in docs
#3354 Total attribute is allowed only on function symbols
#3351 Fixing missing directory in temp container for m2 settings.xml
#3349 Display line numbers for all code blocks
#3346 Move GenSortPredicateRules into the main pipeline
#3342 Add comm attributes to == and =/= operations
#3341 Fix incorrect #token construction for Unicode characters
#3338 Pt.1 change to push location for mvn packages
#3332 Fix github-script v6 breakage
#3331 LSP completion: don't insert whitespaces around parens
#3330 Update release.yml
#3328 add tutorial lesson 2.1
#3324 Provide better documentation for concrete and symbolic attributes
#3323 Fix artifact names on upload
#3319 Fix release tarball upload
#3315 Use gh to simplify uploading release
#3314 Add flag to disable antiLeft priority predicates in KORE
#3313 Remove KBMC and other dead code
#3312 Set release name earlier in release workflow
#3311 Remove kprove module properly
#3310 Set release title with gh release creation
#3309 Correct tar command for producing release
#3308 .github/master-push: fix file name
#3302 Speculative fix for macOS release timeouts
#3299 Switch K master job over to GH Runners
#3296 Update timeout
#3293 Use longer timeouts in release workflow
#3292 Improve lesson 1_08 exercise 2 to point to the source README.md
#3289 Add check that labels provided to --concrete-rules correspond to actual rules
#3288 Deleting axiom production when the it doesn't have any terms.
#3287 Add warning messages when kompiled def is missing
#3282 Add timeouts to release job
#3279 Drop kprove-legacy
#3278 Improve regression-new/help
#3277 Correct documentation on simplification attribute
#3275 Re-export kore-rpc server with K
#3272 Install C binding headers in Nix
#3270 Replacing llvm 14 with llvm 15 as a pre-requirement for K
#3263 Add error message for empty Map collections
#3261 V5.6.0 rc
#3259 Allow bison parsers to be generated as libraries
#3251 Delete the java backend!
#3249 Write external contributors document
#3248 Adopt #3192 for CI
#3244 Remove references to java backend from main regression test suite
#3243 Update FUN and LOGIK
#3242 Update pl-tutorial/1_k/5_types
#3239 Workflow/enable community workflow checks
#3238 Add g++ to dependencies on debian systems
#3230 Automatically use --no-haskell-binary in macOS regression tests
#3229 Update documentation for new LLDB support
#3217 Fixes for mac install of kup
#3216 Revert "make K work with Java 19"
#3215 Updated README to add fmt as an install prerequisite
#3213 disable some modules in the maude backend for the time being
#3212 Change invocation of lldb
#3207 Add flag to enable LLVM backend debugging
#3206 make K work with Java 19
#3205 Updating cachix references for building ghc
#3201 Fix Nix upgrade breaking cachix
#3199 Update kool to use llvm backend and fix warnings
#3198 Fix loc info for gen config cells
#3197 Update deps GH workflow
#3196 Add new flag '--no-pattern' to krun to skip kore-match-disjunction
#3195 Tut fix typofix addedlink
#3194 Add K-Javalette
#3190 .github/: update nix/cachix actions
#3186 Exclude nix result dir from checkstyle
#3184 Add line numbers to the debugging tutorial
#3183 Fix issue with special characters in path
#3182 Fix path to k-exercises repo
#3181 Update simple to llvm backend
#3176 [K MD Parser] Extend TagSelector to Support Line Numbers in Code Blocks
#3174 Fix another batch of suggestions from Clarity on tutorial lessons
#3173 Add selection range in lsp
#3171 Run llvm-kompile using relative paths
#3162 Update Imp++ to use LLVM and Haskell backends
#3160 Fix some of the issues from Clarity on tutorial lessons
#3158 ci: Removed web-related in Dockerfile
#3157 Make gh-pages an orphan branch
#3153 Fix github set-output files
#3151 Add codeowners for version file
#3149 Add proper error message
#3142 Klsp inner
#3136 Depend on libboost-dev for bindings build
#3135 Find occurances
#3131 Add tabstop completion
#3130 Emphasize kup
#3128 add maude backend to KompileOptions
#3126 Make Set concat partial
#3124 Number claims in kprove
#3123 Klsp go to definition
#3118 Fix copyright check
#3117 remove dead code
#3116 Address homebrew enthusiastically upgrading the runner environment
#3115 Expand on direnv instructions
#3113 Install fmt on arch
#3109 some minor tweaks to existing backends
#3107 Build docker images in ${SUBDIR} context
#3104 Lsp
#3103 Add KAVM and KPlutus to the active projects webpage
#3102 Add FMT as a dependency
#3063 Better labels for heat/cool rules of a context
#3032 disable comm axiom generation

PR listing script:

gh pr list                      \
  --repo runtimeverification/k  \
  -s merged                     \
  -L 1000                       \
  --json url,mergedAt,title |
jq -r                           \
  --arg start '2023-01-01'      \
  --arg end '2023-12-31'        \
  '.[] | select(.mergedAt | . >= $start and . <= $end) | select(.title | contains("Update dependency") | not) | .url + " " + .title'