K语言入门学习1：环境搭建

写在前面

1. K是个语义框架，所以它是用来创建一个语言体系的；
2. K本身就是一个语言体系，基于该语言体系，我们将：
   • 创建编程语言
   • 构建类型系统
   • 编写形式化分析工具
3. K语言能够实现以上功能是基于配置和规则：

• 配置会基于cells来组织状态；
• 规则则用来限定词汇的可读、可写、可读可写，或无用等属性。

4. 计算机语言其实就是基于语言抽象语法，按某种句法构成的一件件计算任务，它也是现实事务的一种解释方式；这点与K语言是完全吻合的；也使得K语言特别适合计算机程序这种控制密集型语言，用另一种语言逻辑来验证：

• 可能会突然终止；
• 可能发生异常
• 可能调用等

安装K框架包

工欲善其事，必先利其器。让我们先来把工具安装和环境搭建好。

基于ubuntu辅助工具的安装

选定Ubuntu为K框架的执行的环境。我们所用的Ubuntu是安装在Windows 10的VM Workstation虚拟机上。下面是该Ubuntu的版本：

因此后面选择K框架的包，也选择与该版本相吻合的。

先确认以下的包是否已经安装好：

1. wget：该工具用来获取远程的安装包。
   

2. git：该工具用来访问远程的git仓库。

   [外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-VX8qV6Ie-1652019971203)(C:\Users\Admin\AppData\Roaming\Typora\typora-user-images\1651472357625.png)]

3. curl：该工具用来访问远程的服务器资源。
   

4. 由于我们之前安装了Oracle Java6，而KFramework要用的是OpenJDK11，所以这里要有JDK的多个版本共存与切换的问题要注意。
   
   查看之前安装的JDK6所在的位置，记下来，因为下面的配置与切换会用到（vi /etc/profile）：
   

   下面是安装与配置所用JDK的脚本：

   sudo apt-get install openjdk-11-jdk
   
   sudo update-alternatives --install /usr/bin/java java /usr/lib/jvm/java-11-openjdk-amd64/bin/java 700
   sudo update-alternatives --install /usr/bin/javac javac /usr/bin/java java /usr/lib/jvm/java-11-openjdk-amd64/bin/javac 700
   sudo update-alternatives --install /usr/bin/jar jar /usr/bin/java java /usr/lib/jvm/java-11-openjdk-amd64/bin/jar 700
   
   sudo update-alternatives --config java
   

再来查看java的版本(其实，我们在上面安装完optjdk后，Ubuntu缺省就切换到了该版本)：

5. 执行以下命令，安装指定的库：

mkdir kframeworks
git init
git submodule update --init --recursive
sudo apt-get install build-essential m4 openjdk-11-jdk libgmp-dev libmpfr-dev pkg-config flex bison z3 libz3-dev maven python3 cmake gcc clang-10 lld-10 llvm-10-tools zlib1g-dev libboost-test-dev libyaml-dev libjemalloc-dev
curl -sSL https://get.haskellstack.org/ | sh

其中最后haskellstack的安装如下：

下载K框架包

由于我们只是想使用K框架，并不想更新或改造K框架本身，所以我们直接下载K框架的安装包：kframework_5.3.28_amd64_bionic.deb

安装K框架包

sudo apt install ./kframework_5.3.28_amd64_bionic.deb

安装成功后，该包会被安装在：/usr：

测试K框架包

这里测试是验证K框架包是否安装好。

测试的思路就是是从安装的K框架包里，提取K指导语言例子，然后尝试着编译和运行这些例子；如果成功，则意味着K框架包及其环境搭建好了。

1. 将K tutorial拷贝到某一工作目录，例如：

cp -R /usr/share/kframework/pl-tutorial $HOME/kframeworks/pl-tutorial

2. 然后尝试着编译并运行某个例子：

cd $HOME/kframeworks/pl-tutorial/2_languages/1_simple/1_untyped
make kompile
krun tests/diverse/factorial.simple

看到上面的信息输出，那就恭喜了：K框架的环境搭建好了！

配置编辑器

我们选择notepad++作为K语言的编辑器，所以我们就配置该编辑器，让它可以高亮显示K语言的语法。

我们要做的就是，下载上图所示git库中的k_syntax_highlight_nppp.xml，并更新notepad++编辑器：

1. 首先是拉取相应的git库，以便拿到上述的notepad++模板
   

2. 打开notepad++，通过下图菜单，导入K语言的模板
   
   
   

3. 重启notepad++，以检验上面导致的模板有效
   

相关视频

1.K框架系列视频的来由

2.K框架开发环境搭建