From b6587d059286b917a05e6ab7ae9c2ef7126053ed Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 29 Sep 2022 17:29:19 +0000 Subject: [PATCH 01/10] USER_MANUAL => docs/user_manual --- USER_MANUAL.md => docs/user_manual.md | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename USER_MANUAL.md => docs/user_manual.md (100%) diff --git a/USER_MANUAL.md b/docs/user_manual.md similarity index 100% rename from USER_MANUAL.md rename to docs/user_manual.md From ec3dfb1a4a723361d5a0ab2d60408c7e7171684e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 29 Sep 2022 20:18:56 +0000 Subject: [PATCH 02/10] docs/{ktools,user_manual}: split into two documents --- docs/ktools.md | 308 ++++++++++++++++++++++++++++++++++++++++++++ docs/user_manual.md | 306 +------------------------------------------ 2 files changed, 309 insertions(+), 305 deletions(-) create mode 100644 docs/ktools.md diff --git a/docs/ktools.md b/docs/ktools.md new file mode 100644 index 00000000000..0dc2b4e5f42 --- /dev/null +++ b/docs/ktools.md @@ -0,0 +1,308 @@ +K Tools +======= + +Here we document how to use some of the most commonly used K tools. + +Debugging +--------- + +The LLVM Backend has support for integration with GDB. You can run the debugger +on a particular program by passing the `--debugger` flag to krun, or by +invoking the llvm backend interpreter directly. Below we provide a simple +tutorial to explain some of the basic commands supported by the LLVM backend. + +### LLDB Support + +GDB is not well-supported on macOS, particularly on newer OS versions and Apple +Silicon ARM hardware. Consequently, if the `--debugger` option is passed to krun +on macOS, LLDB[^1] is launched instead of GDB. However, the K-specific debugger +scripts that GDB uses have not been ported to LLDB yet, and so the instructions +in the rest of this section will not work. + +### The K Definition + +Here is a sample K definition we will use to demonstrate debugging +capabilities: + +```k +module TEST + imports INT + + configuration foo(5) + rule [test]: I:Int => I +Int 1 requires I 0 -Int I + +endmodule +``` + +You should compile this definition with `--backend llvm -ccopt -g` and without +`-ccopt -O2` in order to use the debugger most effectively. + +### Stepping + +**Important:** When you first run `krun` with option `--debugger`, GDB will +instruct you on how to modify ~/.gdbinit to enable printing abstract syntax +of K terms in the debugger. If you do not perform this step, you can still +use all the other features, but K terms will be printed as their raw address +in memory. GDB will need the kompiled interpreter in its safe path in order +to access the pretty printing python script within it. A good way to do this +would be to pick a minimum top-level path that covers all of your kompiled +semantics (ie. `set auto-load safe-path ~/k-semantics`) + +You can break before every step of execution is taken by setting a breakpoint +on the `step` function: + +``` +(gdb) break definition.kore:step +Breakpoint 1 at 0x25e340 +(gdb) run +Breakpoint 1, 0x000000000025e340 in step (subject=`{}`(`{}`(`kseq{}`(`inj{Int{}, KItem{}}`(#token("0", "Int")),dotk{}(.KList))),`{}`(#token("0", "Int")))) +(gdb) continue +Continuing. + +Breakpoint 1, 0x000000000025e340 in step (subject=`{}`(`{}`(`kseq{}`(`inj{Int{}, KItem{}}`(#token("1", "Int")),dotk{}(.KList))),`{}`(#token("0", "Int")))) +(gdb) continue 2 +Will ignore next crossing of breakpoint 1. Continuing. + +Breakpoint 1, 0x000000000025e340 in step (subject=`{}`(`{}`(`kseq{}`(`inj{Int{}, KItem{}}`(#token("3", "Int")),dotk{}(.KList))),`{}`(#token("0", "Int")))) +(gdb) +``` + +### Breaking on a specific rule + +You can break when a rule is applied by giving the rule a rule label. If the +module name is TEST and the rule label is test, you can break when the rule +applies by setting a breakpoint on the `TEST.test.rhs` function: + +``` +(gdb) break TEST.test.rhs +Breakpoint 1 at 0x25e250: file /home/dwightguth/test/./test.k, line 4. +(gdb) run +Breakpoint 1, TEST.test.rhs (VarDotVar0=`{}`(#token("0", "Int")), VarDotVar1=dotk{}(.KList), VarI=#token("0", "Int")) at /home/dwightguth/test/./test.k:4 +4 rule [test]: I:Int => I +Int 1 requires I I +Int 1 requires I I +Int 1 requires I {}`(#token("0", "Int")), VarDotVar1=dotk{}(.KList), VarI=#token("0", "Int")) at /home/dwightguth/test/./test.k:4 +4 rule [test]: I:Int => I +Int 1 requires I I +Int 1 requires I + breakpoint already hit 3 times +1.1 y 0x000000000025e230 in TEST.test.sc at /home/dwightguth/test/./test.k:4 +1.2 y 0x000000000025e250 in TEST.test.rhs at /home/dwightguth/test/./test.k:4 +(gdb) disable 1.1 +(gdb) continue +Continuing. + +Breakpoint 1, TEST.test.rhs (VarDotVar0=`{}`(#token("0", "Int")), VarDotVar1=dotk{}(.KList), VarI=#token("1", "Int")) at /home/dwightguth/test/./test.k:4 +4 rule [test]: I:Int => I +Int 1 requires I {}`(#token("0", "Int")), VarDotVar1=dotk{}(.KList), VarI=#token("2", "Int")) at /home/dwightguth/test/./test.k:4 +4 rule [test]: I:Int => I +Int 1 requires I {}`(#token("0", "Int")), VarDotVar1=dotk{}(.KList)) at /home/dwightguth/test/./test.k:9 +#2 0x0000000000268a52 in take_steps () +#3 0x000000000026b7b4 in main () +(gdb) +``` + +Here we see that `foo` was invoked while applying the rule on line 9 of test.k, +and we also can see the substitution of that rule. If foo was evaluated while +evaluating another function, we would also be able to see the arguments of that +function as well, unless the function was tail recursive, in which case no +stack frame would exist once the tail call was performed. + +### Breaking on a set of rules or functions + +Using `rbreak ` you can set breakpoints on multiple functions. + +- `rbreak Lbl` - sets a breakpoint on all non hooked `function`s + +- `rbreak Lbl.*TEST` - sets a breakpoint on all `function`s from module `TEST` + +- `rbreak hook_INT` - sets a breakpoint on all hooks from module `INT` + +### Other debugger issues + +- `` try kompiling without `-O1`, `-O2`, or `-O3`. +- `(gdb) break definition.kore:break -> No source file named definition.kore.` +send `-ccopt -g` to kompile in order to generate debug info symbols. + +Profiling your K semantics +-------------------------- + +The first thing to be aware of is in order to get meaningful data, +you need to build the semantics and all of its dependencies with +optimizations enabled but _without the frame pointer elimination +optimization_. For example, for EVM, this means rebuilding GMP, MPFR, +JEMalloc, Crypto++, SECP256K1, etc with the following `exports`. + +```sh +export CFLAGS="-DNDEBUG -O2 -fno-omit-frame-pointer" +export CXXFLAGS="-DNDEBUG -O2 -fno-omit-frame-pointer" +``` + +You can skip this step, but if you do, any samples within these +libraries will not have correct stack trace information, which means +you will likely not get a meaningful set of data that will tell you +where the majority of time is really being spent. Don't worry about +rebuilding literally every single dependency though. Just focus on the +ones that you expect to take a non-negligible amount of runtime. You +will be able to tell if you haven't done enough later, and you can go +back and rebuild more. Once this is done, you then build K with +optimizations and debug info enabled, like so: + +```sh +mvn package -Dproject.build.type="FastBuild" +``` + +Next, you build the semantics with optimizations and debug info +enabled (i.e., `kompile -ccopt -O2 --iterated -ccopt -fno-omit-frame-pointer`). + +Once all this is done, you should be ready to profile your +application. Essentially, you should run whatever test suite you +usually run, but with `perf record -g -- ` prefixed to the front. For +example, for KEVM it's the following command. (For best data, don't +run this step in parallel.) + +```sh +perf record -g -- make test-conformance +``` + +Finally, you want to filter out just the samples that landed within +the llvm backend and view the report. For this, you need to know the +name of the binary that was generated by your build system. Normally +it is `interpreter`, but e.g. if you are building the web3 client for +kevm, it would be `kevm-client`. You will want to run the following +command. + +```sh +perf report -g -c $binary_name +``` + +If all goes well, you should see a breakdown of where CPU time has +been spent executing the application. You will know that sufficient +time was spent rebuilding dependencies with the correct flags when the +total time reported by the main method is close to 100%. If it's not +close to 100%, this is probably because a decent amount of self time +was reported in stack traces that were not built with frame pointers +enabled, meaning that perf was unable to walk the stack. You will have +to go back, rebuild the appropriate libraries, and then record your +trace again. + +Your ultimate goal is to identify the hotspots that take the most +time, and make them execute faster. Entries like `step` and +`step_1234` like functions refer to the cost of matching. An entry +like `side_condition_1234` is a side condition and `apply_rule_1234` +is constructing the rhs of a rule. You can convert from this rule +ordinal to a location using the `llvm-kompile-compute-loc` script in +the bin folder of the llvm backend repo. For example, + +```sh +llvm-kompile-compute-loc 5868 evm-semantics/.build/defn/llvm/driver-kompiled +``` + +spits out the following text. + +``` +Line: 18529 +/home/dwightguth/evm-semantics/./.build/defn/llvm/driver.k:493:10 +``` + +This is the line of `definition.kore` that the axiom appears on as +well as the original location of the rule in the K semantics. You can +use this information to figure out which rules and functions are +causing the most time and optimize them to be more efficient. diff --git a/docs/user_manual.md b/docs/user_manual.md index 71a8cd01841..90b813d934d 100644 --- a/docs/user_manual.md +++ b/docs/user_manual.md @@ -870,7 +870,7 @@ module WIDGET [private] // module // this production is visible outside this module - syntax KItem ::= adjustWidget(Widget) [function, public] + syntax KItem ::= adjustWidget(Widget) [function, public] endmodule ``` @@ -2824,310 +2824,6 @@ the number of terminals in the production plus the number of `%c` substrings in the `format` attribute. -Debugging ---------- - -The LLVM Backend has support for integration with GDB. You can run the debugger -on a particular program by passing the `--debugger` flag to krun, or by -invoking the llvm backend interpreter directly. Below we provide a simple -tutorial to explain some of the basic commands supported by the LLVM backend. - -### LLDB Support - -GDB is not well-supported on macOS, particularly on newer OS versions and Apple -Silicon ARM hardware. Consequently, if the `--debugger` option is passed to krun -on macOS, LLDB[^1] is launched instead of GDB. However, the K-specific debugger -scripts that GDB uses have not been ported to LLDB yet, and so the instructions -in the rest of this section will not work. - -### The K Definition - -Here is a sample K definition we will use to demonstrate debugging -capabilities: - -```k -module TEST - imports INT - - configuration foo(5) - rule [test]: I:Int => I +Int 1 requires I 0 -Int I - -endmodule -``` - -You should compile this definition with `--backend llvm -ccopt -g` and without -`-ccopt -O2` in order to use the debugger most effectively. - -### Stepping - -**Important:** When you first run `krun` with option `--debugger`, GDB will -instruct you on how to modify ~/.gdbinit to enable printing abstract syntax -of K terms in the debugger. If you do not perform this step, you can still -use all the other features, but K terms will be printed as their raw address -in memory. GDB will need the kompiled interpreter in its safe path in order -to access the pretty printing python script within it. A good way to do this -would be to pick a minimum top-level path that covers all of your kompiled -semantics (ie. `set auto-load safe-path ~/k-semantics`) - -You can break before every step of execution is taken by setting a breakpoint -on the `step` function: - -``` -(gdb) break definition.kore:step -Breakpoint 1 at 0x25e340 -(gdb) run -Breakpoint 1, 0x000000000025e340 in step (subject=`{}`(`{}`(`kseq{}`(`inj{Int{}, KItem{}}`(#token("0", "Int")),dotk{}(.KList))),`{}`(#token("0", "Int")))) -(gdb) continue -Continuing. - -Breakpoint 1, 0x000000000025e340 in step (subject=`{}`(`{}`(`kseq{}`(`inj{Int{}, KItem{}}`(#token("1", "Int")),dotk{}(.KList))),`{}`(#token("0", "Int")))) -(gdb) continue 2 -Will ignore next crossing of breakpoint 1. Continuing. - -Breakpoint 1, 0x000000000025e340 in step (subject=`{}`(`{}`(`kseq{}`(`inj{Int{}, KItem{}}`(#token("3", "Int")),dotk{}(.KList))),`{}`(#token("0", "Int")))) -(gdb) -``` - -### Breaking on a specific rule - -You can break when a rule is applied by giving the rule a rule label. If the -module name is TEST and the rule label is test, you can break when the rule -applies by setting a breakpoint on the `TEST.test.rhs` function: - -``` -(gdb) break TEST.test.rhs -Breakpoint 1 at 0x25e250: file /home/dwightguth/test/./test.k, line 4. -(gdb) run -Breakpoint 1, TEST.test.rhs (VarDotVar0=`{}`(#token("0", "Int")), VarDotVar1=dotk{}(.KList), VarI=#token("0", "Int")) at /home/dwightguth/test/./test.k:4 -4 rule [test]: I:Int => I +Int 1 requires I I +Int 1 requires I I +Int 1 requires I {}`(#token("0", "Int")), VarDotVar1=dotk{}(.KList), VarI=#token("0", "Int")) at /home/dwightguth/test/./test.k:4 -4 rule [test]: I:Int => I +Int 1 requires I I +Int 1 requires I - breakpoint already hit 3 times -1.1 y 0x000000000025e230 in TEST.test.sc at /home/dwightguth/test/./test.k:4 -1.2 y 0x000000000025e250 in TEST.test.rhs at /home/dwightguth/test/./test.k:4 -(gdb) disable 1.1 -(gdb) continue -Continuing. - -Breakpoint 1, TEST.test.rhs (VarDotVar0=`{}`(#token("0", "Int")), VarDotVar1=dotk{}(.KList), VarI=#token("1", "Int")) at /home/dwightguth/test/./test.k:4 -4 rule [test]: I:Int => I +Int 1 requires I {}`(#token("0", "Int")), VarDotVar1=dotk{}(.KList), VarI=#token("2", "Int")) at /home/dwightguth/test/./test.k:4 -4 rule [test]: I:Int => I +Int 1 requires I {}`(#token("0", "Int")), VarDotVar1=dotk{}(.KList)) at /home/dwightguth/test/./test.k:9 -#2 0x0000000000268a52 in take_steps () -#3 0x000000000026b7b4 in main () -(gdb) -``` - -Here we see that `foo` was invoked while applying the rule on line 9 of test.k, -and we also can see the substitution of that rule. If foo was evaluated while -evaluating another function, we would also be able to see the arguments of that -function as well, unless the function was tail recursive, in which case no -stack frame would exist once the tail call was performed. - -### Breaking on a set of rules or functions - -Using `rbreak ` you can set breakpoints on multiple functions. - -- `rbreak Lbl` - sets a breakpoint on all non hooked `function`s - -- `rbreak Lbl.*TEST` - sets a breakpoint on all `function`s from module `TEST` - -- `rbreak hook_INT` - sets a breakpoint on all hooks from module `INT` - -### Other debugger issues - -- `` try kompiling without `-O1`, `-O2`, or `-O3`. -- `(gdb) break definition.kore:break -> No source file named definition.kore.` -send `-ccopt -g` to kompile in order to generate debug info symbols. - -Profiling your K semantics --------------------------- - -The first thing to be aware of is in order to get meaningful data, -you need to build the semantics and all of its dependencies with -optimizations enabled but _without the frame pointer elimination -optimization_. For example, for EVM, this means rebuilding GMP, MPFR, -JEMalloc, Crypto++, SECP256K1, etc with the following `exports`. - -```sh -export CFLAGS="-DNDEBUG -O2 -fno-omit-frame-pointer" -export CXXFLAGS="-DNDEBUG -O2 -fno-omit-frame-pointer" -``` - -You can skip this step, but if you do, any samples within these -libraries will not have correct stack trace information, which means -you will likely not get a meaningful set of data that will tell you -where the majority of time is really being spent. Don't worry about -rebuilding literally every single dependency though. Just focus on the -ones that you expect to take a non-negligible amount of runtime. You -will be able to tell if you haven't done enough later, and you can go -back and rebuild more. Once this is done, you then build K with -optimizations and debug info enabled, like so: - -```sh -mvn package -Dproject.build.type="FastBuild" -``` - -Next, you build the semantics with optimizations and debug info -enabled (i.e., `kompile -ccopt -O2 --iterated -ccopt -fno-omit-frame-pointer`). - -Once all this is done, you should be ready to profile your -application. Essentially, you should run whatever test suite you -usually run, but with `perf record -g -- ` prefixed to the front. For -example, for KEVM it's the following command. (For best data, don't -run this step in parallel.) - -```sh -perf record -g -- make test-conformance -``` - -Finally, you want to filter out just the samples that landed within -the llvm backend and view the report. For this, you need to know the -name of the binary that was generated by your build system. Normally -it is `interpreter`, but e.g. if you are building the web3 client for -kevm, it would be `kevm-client`. You will want to run the following -command. - -```sh -perf report -g -c $binary_name -``` - -If all goes well, you should see a breakdown of where CPU time has -been spent executing the application. You will know that sufficient -time was spent rebuilding dependencies with the correct flags when the -total time reported by the main method is close to 100%. If it's not -close to 100%, this is probably because a decent amount of self time -was reported in stack traces that were not built with frame pointers -enabled, meaning that perf was unable to walk the stack. You will have -to go back, rebuild the appropriate libraries, and then record your -trace again. - -Your ultimate goal is to identify the hotspots that take the most -time, and make them execute faster. Entries like `step` and -`step_1234` like functions refer to the cost of matching. An entry -like `side_condition_1234` is a side condition and `apply_rule_1234` -is constructing the rhs of a rule. You can convert from this rule -ordinal to a location using the `llvm-kompile-compute-loc` script in -the bin folder of the llvm backend repo. For example, - -```sh -llvm-kompile-compute-loc 5868 evm-semantics/.build/defn/llvm/driver-kompiled -``` - -spits out the following text. - -``` -Line: 18529 -/home/dwightguth/evm-semantics/./.build/defn/llvm/driver.k:493:10 -``` - -This is the line of `definition.kore` that the axiom appears on as -well as the original location of the rule in the K semantics. You can -use this information to figure out which rules and functions are -causing the most time and optimize them to be more efficient. - Attributes Reference -------------------- From 27efcebaf81c76e420e47a40dd34fd8002e958eb Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 29 Sep 2022 20:21:12 +0000 Subject: [PATCH 03/10] docs/cheat-sheet: add initial cheat sheet --- docs/cheat_sheet.md | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 docs/cheat_sheet.md diff --git a/docs/cheat_sheet.md b/docs/cheat_sheet.md new file mode 100644 index 00000000000..2004bba372b --- /dev/null +++ b/docs/cheat_sheet.md @@ -0,0 +1,26 @@ +K Cheat Sheet +============= + +This is a quick reference of the most commonly used K tools. + +``` +kompile (--gen-bison-parser)? {file} : generate parser, optionally with ahead of time +krun {file} : interpret file +krun -cPGM='{string}' : interpret string +kast --output (kore | kast) (-e|{file}) : parse expression or file +kompile (--enable-search --backend haskell)? {file} : generate parser, enabling non-deterministic run +krun (--search-all)? {file} : interpret file, evaluating non-deterministic runs as well +foo-kompiled/parser_PGM {file} : ahead of time parse +kompile (--main-module)? (--syntax-module)? {file} : generate parser for {file}.k {file}-syntax.k, explicitly state main modules +kparse | kore-print - : parse and unparse a file +kompile {file} -ccopt -g -ccopt -O1 : generate debuggable output for {file}.k +krun {file} --debugger : debug K code +kprove {file} : Verify specs in {file} +``` + +Durring GDB debugging session: + +``` +break {file}:{linenum} : add a breakpoint to {file}'s {linenum} numbered line +k match {module}.{label} subject : investigate matching +``` From 643af8f934cee0bc00b7ef0624f01bdbf86981c5 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 29 Sep 2022 20:29:56 +0000 Subject: [PATCH 04/10] web/pages/index: update the structure of the front page --- web/pages/index.md | 33 ++++++++++++++++++--------------- 1 file changed, 18 insertions(+), 15 deletions(-) diff --git a/web/pages/index.md b/web/pages/index.md index 6ec89f8ffeb..e111f9138a7 100644 --- a/web/pages/index.md +++ b/web/pages/index.md @@ -14,13 +14,6 @@ another, modified, or deleted. This makes K suitable for defining control-intensive features such as abrupt termination, exceptions, or call/cc. -## Overview - -- A ten-minute overview video [slide presentation](./overview.md). -- A ninety-minute [tutorial video](https://youtu.be/3ovulLNCEQc?list=PLQMvp5V6ZQjOm4JZK15s-WJtQHxOmb2h7), given at ETAPS'16. -- [Optional] A high-level [interview](http://channel9.msdn.com/posts/ICSE-2011-Grigore-Rosu-The-Art-and-Science-of-Program-Verification) about rewrite-based semantics (Wolfram Schulte interviews Grigore Rosu at [ICSE'11](http://2011.icse-conferences.org/). -- [FAQ](./faq.md) - ## K Tool Download - The provided [K Tool Binaries](./downloads.md) are supported on Linux, OS X, and Windows. Other platforms may or may not work correctly. We welcome information about usability of unsupported platforms or bugs in the supported platforms. @@ -29,14 +22,24 @@ call/cc. ## Learn K -- Do the K Tutorial! -- Read some papers about K on the [Formal Systems Laboratory (FSL)](https://fsl.cs.illinois.edu/publications/). -- User documentation -- Builtins +- Do the K Tutorial! +- Build programming languages in K! +- Reference Documentation +- K Cheat Sheet +- K Tool Reference +- K Builtins -## Links +## Support -- [K webpage](http://fmse.info.uaic.ro/projects/K/) at UAIC (Romania). +- [Discord Server](https://discord.gg/HygNq4QY): Most direct way to get support. +- [Matrix Room](https://riot.im/app/#/room/#k:matrix.org): Another way to get support. +- [Stackoverflow](https://stackoverflow.com/questions/tagged/kframework): for general questions to the K user community. + +## Resources + +- Read some papers about K on the [Formal Systems Laboratory (FSL)](https://fsl.cs.illinois.edu/publications/). - [Matching logic](http://matching-logic.org/) webpage at UIUC (USA). -- [Online K Discussion Channel](https://riot.im/app/#/room/#k:matrix.org) for K users (Slack & Riot). This is the recommended way to ask questions about K and interact with the K community. -- [Stackoverflow](https://stackoverflow.com/questions/tagged/kframework) for general questions to the K user community (use the channel above if you want quick answers). +- A ten-minute overview video [slide presentation](./overview.md). +- A ninety-minute [tutorial video](https://youtu.be/3ovulLNCEQc?list=PLQMvp5V6ZQjOm4JZK15s-WJtQHxOmb2h7), given at ETAPS'16. +- [Optional] A high-level [interview](http://channel9.msdn.com/posts/ICSE-2011-Grigore-Rosu-The-Art-and-Science-of-Program-Verification) about rewrite-based semantics (Wolfram Schulte interviews Grigore Rosu at [ICSE'11](http://2011.icse-conferences.org/). +- [FAQ](./faq.md) From 44f7411ad4f5ede6e594ce99f86f3faf50d2cbf6 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 29 Sep 2022 20:31:44 +0000 Subject: [PATCH 05/10] web/toc; update TOC --- web/toc.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/web/toc.md b/web/toc.md index e71035410db..eb2771f6991 100644 --- a/web/toc.md +++ b/web/toc.md @@ -40,6 +40,7 @@ output: - [Lesson 1.19: Debugging with GDB](/k-distribution/k-tutorial/1_basic/19_debugging/README.md) - [Lesson 1.20: K Backends and the Haskell Backend](/k-distribution/k-tutorial/1_basic/20_backends/README.md) - [Lesson 1.21: Unification and Symbolic Execution](/k-distribution/k-tutorial/1_basic/21_symbolic_execution/README.md) + - [Lesson 1.22: K Deductive Verification](/k-distribution/k-tutorial/1_basic/22_proofs/README.md) - [K PL Tutorial](/k-distribution/pl-tutorial/README.md) - [K Overview](/web/pages/overview.md) - [Learning K](/k-distribution/pl-tutorial/1_k/README.md) @@ -100,7 +101,9 @@ output: - Lesson 3, FUN polymorphic type inferencer - [Part 10: LOGIK: Designing Logic Programming Languages](/k-distribution/pl-tutorial/2_languages/4_logik/basic/logik.md) - [Lesson 1, LOGIK](/k-distribution/pl-tutorial/2_languages/4_logik/basic/logik.md) -- [K User Manual](/USER_MANUAL.md) +- [K User Manual](/docs/user_manual.md) +- [K Cheat Sheet](/docs/cheat_sheet.md) +- [K Tool Reference](/docs/ktools.md) - [K Builtins](/k-distribution/include/kframework/builtin/README.md) - [domains](/k-distribution/include/kframework/builtin/domains.md) - [kast](/k-distribution/include/kframework/builtin/kast.md) From 6160978d18869d1fa4cad18b55b9f9acc9969ee6 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 29 Sep 2022 20:32:24 +0000 Subject: [PATCH 06/10] web/toc: move K PL Tutorial further down the list --- web/toc.md | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/web/toc.md b/web/toc.md index eb2771f6991..56937c20716 100644 --- a/web/toc.md +++ b/web/toc.md @@ -41,6 +41,18 @@ output: - [Lesson 1.20: K Backends and the Haskell Backend](/k-distribution/k-tutorial/1_basic/20_backends/README.md) - [Lesson 1.21: Unification and Symbolic Execution](/k-distribution/k-tutorial/1_basic/21_symbolic_execution/README.md) - [Lesson 1.22: K Deductive Verification](/k-distribution/k-tutorial/1_basic/22_proofs/README.md) +- [K User Manual](/docs/user_manual.md) +- [K Cheat Sheet](/docs/cheat_sheet.md) +- [K Tool Reference](/docs/ktools.md) +- [K Builtins](/k-distribution/include/kframework/builtin/README.md) + - [domains](/k-distribution/include/kframework/builtin/domains.md) + - [kast](/k-distribution/include/kframework/builtin/kast.md) + - [prelude](/k-distribution/include/kframework/builtin/prelude.md) + - [ffi](/k-distribution/include/kframework/builtin/ffi.md) + - [json](/k-distribution/include/kframework/builtin/json.md) + - [rat](/k-distribution/include/kframework/builtin/rat.md) + - [substitution](/k-distribution/include/kframework/builtin/substitution.md) + - [unification](https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/unification.k) - [K PL Tutorial](/k-distribution/pl-tutorial/README.md) - [K Overview](/web/pages/overview.md) - [Learning K](/k-distribution/pl-tutorial/1_k/README.md) @@ -101,18 +113,6 @@ output: - Lesson 3, FUN polymorphic type inferencer - [Part 10: LOGIK: Designing Logic Programming Languages](/k-distribution/pl-tutorial/2_languages/4_logik/basic/logik.md) - [Lesson 1, LOGIK](/k-distribution/pl-tutorial/2_languages/4_logik/basic/logik.md) -- [K User Manual](/docs/user_manual.md) -- [K Cheat Sheet](/docs/cheat_sheet.md) -- [K Tool Reference](/docs/ktools.md) -- [K Builtins](/k-distribution/include/kframework/builtin/README.md) - - [domains](/k-distribution/include/kframework/builtin/domains.md) - - [kast](/k-distribution/include/kframework/builtin/kast.md) - - [prelude](/k-distribution/include/kframework/builtin/prelude.md) - - [ffi](/k-distribution/include/kframework/builtin/ffi.md) - - [json](/k-distribution/include/kframework/builtin/json.md) - - [rat](/k-distribution/include/kframework/builtin/rat.md) - - [substitution](/k-distribution/include/kframework/builtin/substitution.md) - - [unification](https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/unification.k) - [Projects using K](/web/pages/projects.md) From 57963d062a30cb3e032cda225823a2ed759a9e5a Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 29 Sep 2022 20:33:38 +0000 Subject: [PATCH 07/10] web/build-html: build all the docs --- web/build-html.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/web/build-html.js b/web/build-html.js index acc385beccd..e5c81453efb 100644 --- a/web/build-html.js +++ b/web/build-html.js @@ -51,7 +51,7 @@ generatePagesFromMarkdownFiles({ }, }); generatePagesFromMarkdownFiles({ - globPattern: path.resolve(__dirname, "../") + "/USER_MANUAL.md", + globPattern: path.resolve(__dirname, "../docs") + "*.md", globOptions: {}, origin: "https://github.com/runtimeverification/k/tree/master/", sourceDirectory: path.resolve(__dirname, "../"), From b838706dc9d5d5e5d0fb63fe15c24b5bb96ae1c5 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 29 Sep 2022 20:46:50 +0000 Subject: [PATCH 08/10] web/: link directly to GitHub release for installs --- web/pages/downloads.md | 3 --- web/pages/index.md | 6 +++--- web/static_content/html/include/header.html | 2 +- web/toc.md | 2 +- 4 files changed, 5 insertions(+), 8 deletions(-) delete mode 100644 web/pages/downloads.md diff --git a/web/pages/downloads.md b/web/pages/downloads.md deleted file mode 100644 index d471cf835f0..00000000000 --- a/web/pages/downloads.md +++ /dev/null @@ -1,3 +0,0 @@ -# K Tool Binaries - -Download the latest [stable release](https://github.com/runtimeverification/k/releases/latest) or prior [releases](https://github.com/runtimeverification/k/releases). diff --git a/web/pages/index.md b/web/pages/index.md index e111f9138a7..7eaee328ff6 100644 --- a/web/pages/index.md +++ b/web/pages/index.md @@ -16,13 +16,13 @@ call/cc. ## K Tool Download -- The provided [K Tool Binaries](./downloads.md) are supported on Linux, OS X, and Windows. Other platforms may or may not work correctly. We welcome information about usability of unsupported platforms or bugs in the supported platforms. +- Install from the latest [K GitHub Release](https://github.com/runtimeverification/k/releases/latest). - Try our [Editor Support](./editor_support.md) page for links to K syntax highlighting definitions for various popular editors/IDEs. Please feel free to contribute. -- The source code (Java) is available on [GitHub](https://github.com/kframework), where you can also [report bugs](http://github.com/runtimeverification/k/issues) (please do so). +- Build or browse the code [on GitHub](https://github.com/kframework), where you can also [report bugs](http://github.com/runtimeverification/k/issues). ## Learn K -- Do the K Tutorial! +- Do the K Tutorial! - Build programming languages in K! - Reference Documentation - K Cheat Sheet diff --git a/web/static_content/html/include/header.html b/web/static_content/html/include/header.html index 45da6ffd953..4ecf8df6ec5 100644 --- a/web/static_content/html/include/header.html +++ b/web/static_content/html/include/header.html @@ -45,7 +45,7 @@ Download diff --git a/web/toc.md b/web/toc.md index 56937c20716..5d5e3b7ba7b 100644 --- a/web/toc.md +++ b/web/toc.md @@ -16,7 +16,7 @@ output: # Table of Contents - [Homepage](/web/pages/index.md) -- [K Tool Binaries](/web/pages/downloads.md) +- [Install K](https://github.com/runtimeverification/k/releases/latest) - [K Tutorial](/k-distribution/k-tutorial/README.md) - [Section 1: Basic K Concepts](/k-distribution/k-tutorial/1_basic/README.md) - [Lesson 1.1: Setting up a K Environment](/k-distribution/k-tutorial/1_basic/01_installing/README.md) From d4734b3bc75eae0c37208dfc7e3d5f4b7b140ee3 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 29 Sep 2022 20:51:39 +0000 Subject: [PATCH 09/10] web/pages/index: fix URL --- web/pages/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/web/pages/index.md b/web/pages/index.md index 7eaee328ff6..5a033416eec 100644 --- a/web/pages/index.md +++ b/web/pages/index.md @@ -18,7 +18,7 @@ call/cc. - Install from the latest [K GitHub Release](https://github.com/runtimeverification/k/releases/latest). - Try our [Editor Support](./editor_support.md) page for links to K syntax highlighting definitions for various popular editors/IDEs. Please feel free to contribute. -- Build or browse the code [on GitHub](https://github.com/kframework), where you can also [report bugs](http://github.com/runtimeverification/k/issues). +- Build or browse the code [on GitHub](https://github.com/runtimeverification/k), where you can also [report bugs](http://github.com/runtimeverification/k/issues). ## Learn K From c5d0e9febbc90b42175268a39dacd891900672fa Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 29 Sep 2022 20:56:36 +0000 Subject: [PATCH 10/10] web/build-html.js: correct glob --- web/build-html.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/web/build-html.js b/web/build-html.js index e5c81453efb..65b945d5bb0 100644 --- a/web/build-html.js +++ b/web/build-html.js @@ -51,7 +51,7 @@ generatePagesFromMarkdownFiles({ }, }); generatePagesFromMarkdownFiles({ - globPattern: path.resolve(__dirname, "../docs") + "*.md", + globPattern: path.resolve(__dirname, "../docs/") + "/*.md", globOptions: {}, origin: "https://github.com/runtimeverification/k/tree/master/", sourceDirectory: path.resolve(__dirname, "../"),