K version bump feature list (5.2.0)

[ehildenb]

• Features:
  • Deprecated imports syntax: [KIP] - Deprecate imports syntax ($SYNTAX modules) #1851
  • Constant folding kompiler pass: Constant folding of Int, Float, String, and Bool #1896, Revert "Constant folding of Int, Float, String, and Bool" #1946, Fix constant folding PR quadratic behavior #1958
  • MAP module is automatically imported into all modules that declare configurations: Add MAP import to all modules containing configs #1965
  • krun --search supported in LLVM backend: Search in llvm backend #1978
  • add #let A = B #in C syntax #2082
  • kprovex: Lightweight Kprove - 2 #2089
  • Module signatures supporting public/private syntax and imports #1658
  • More verbose information #2164
  • Expose pyk term minimizer to command line #2199
  • Rework timing info for --profile-rule-parsing #2204
  • Add #kompiledDirectory hook to K-REFLECTION #2209
  • K-REFLECTION: add #unparseKORE hook #2214
  • Expose floating-point truncation hook #2218
  • Declare encoding/decoding between Bytes and String in domains.md #2002
  • Allow putting macro on productions #1584
  • imports FOO.bar with fixed OOM #2292
• Documentation updates:
  • Document version requirements for dependencies #1706
  • Clarify the symbol attribute in the pending document #1777
  • K tutorial through lesson 12: lessons 3/4: parsing and disambiguation #1847 Lesson 5: modules, imports, and requires #1973 Lesson 6: integers and booleans #1992 Lesson 7: Side conditions and rule priority #1993 Lesson 8: Literate Programming #1994 Lesson 9: unparsing and formatting #2005 Lesson 10: Strings #2011 Lesson 11: Casts #2018 Lesson 12: syntactic lists #2023
  • Add documentation for restrictions on simplification rules #1926
  • Documentation update for symbol, klabel, simplification, and Z3 version #1930
  • Update pending-documentation.md: side conditions are supported for smt-lemma rules #1995
  • Merge --help and --help-experimental, remove defunct options. #1684
  • Improve error message for ambiguous parses #1968
  • [Bug] kompile - [Error] Critical: llvm-kompile returned nonzero exit code: 127 #1955
  • Rename pending-documentation.md to USER_MANUAL.md #2054
  • relicense as BSD 3 clause #2059
  • Add attribute reference to the user manual #2127
• Bug fixes:
  • [Bug] kompile - Inconsistent symlink handling in require #1906
  • kast ignores the parameter --output-file #1088
  • [Bug] kompile - suggests to add existing attribute (simplification) #1940
  • [KIP] - --no-exc-wrap flag for krun #1990
  • Outer parsing is very slow on very large comments #1967
  • ConstantFoldingTest.testFloat2String() fails because of locale #1969
  • Update Location of cached Bubbles #2001
  • Check cell sorts #2071
  • add structural errors for misuse of binder attribute #2092
  • Outer: remove redundancy in parser error message #2102
  • fix krun script to use module specified by module attribute for kparse #2123
  • Redirect kprove test output to stdout #2153
  • report better error if bison parsing fails #2160
  • Update parser error messages, second draft #2161
  • Implement -I, --md-selector, and --no-prelude in kprove, kprovex, keq, and kbmc #2172
  • Include git describe in output of kompile --version #2184
  • Add check for search executable in krun #2203
  • Record prods macros #2226
  • kprint: fix printing of append in KoreToK #2266
  • Kompile: add check for existential variable in LHS #2280
• Performance improvements:
  • Optimize POSet performance #1944
  • optimize array extensions #1952
  • Parse configs in parallel #1996
  • refactor krun to use new parsing scripts #2060
  • Parse record productions in linear time #2012
  • Anonymous variables get their type directly #2271
• Dependencies
  • Switched to java serialization: Fix lock contention during serialization and deserialization when using kserver #2050 Use BufferedStreams in serialization #2051
  • LLVM version 10: README: add minimum version for clang, lldb, and llvm #2049, update minimum llvm version #2213
  • Scala: scala version bump #2189

Check:

• File ./package/version has been bumped to NEW_MAJOR.NEW_MINOR.0, and ./package/version.sh sub has been invoked.
• CHANGELOG.md has been updated with new features.
• krun help script is correctly reflecting the available options
• All *Options.java files are up-to-date.
• K active projects page is up-to-date (receiving commits in the last 3 months).
• Audit of warnings in regression test-suite and tutorial.
• Audit package dependencies in package/.