基于coq平台形式化编译过程说明

编译文件的作用是使文件编译成为类似c语言库文件的过程。在其他文件中进行引用的文件必须进行编译过程，举个例子进行说明。

图1-1

图1-1文件中的uart.v的文件是某代码的coq语言表示，打开该文件后如图1-2。

如图1-2

当我们在其他文件中需要引用到coq语言表示的uart.v代码时，就必须对uart.v进行编译。

编译的操作步骤如下：

步骤一：使用终端Cd到包含uart.v文件的目录下，如本系统的目录如图就是 /home/cav/Documents/AGOS

图1-3

Cd命令后的效果如图1-4。

图1-4

步骤二：使用coqc uart.v命令进行uart.v文件的编译工作。编译完成后产生两个文件uart.glob和uart.vo。其中uart.vo就是编译后的文件如图1-5。

图1-5

说明编译成功，编译成功的前提是没有uart.v里面的代码没有语法错误。当我们在文件uart_os_program.v中使用到uart.v中定义的变量，函数名等信息时，直接使用命令Require Import uart.即可在文件uart_os_program.v引用文件uart.v定义的内容如图1-6。

图1-6