为以后保存我的跑步顶级

用户 HOL light 有类似的需求,他们使用检查点程序来保存顶级的快照。见 this message 在CAML邮件列表中,或第8页,共页 this HOL tutorial .

一般来说,最好将定义保留为源代码,而不是二进制顶级快照。许多工具允许快速将.ml文件加载到顶层,以方便实验(Emacs模式等)。请参见HOL教程中的警告:

在hol中开发大型证明时,应该始终将证明脚本保持为 准备重新加载的OCAML文件,而不是依赖于CKPT。这将允许证据 以后再修改,供他人使用等,但制作起来很方便 中间快照,这样您就不必加载大文件来进一步处理证据。 这类似于编程中的常见情况:您应该始终保持 完成源代码,但不希望每次使用时重新编译所有源 代码。

至少在OCAML中没有内置的支持。解决方案是使用 rlwrap 或任何其他的readline包装器,用于将输入的历史记录记录到文件中。例如:

> rlwrap -H mysession.ml ocaml

缺点是,它还将记录有语法错误的输入,因此您必须清除这些错误。请注意,默认情况下,如果不使用-h选项调用rlwrap,它将自动将输入保存到~/.ocaml_历史记录中。

在哈斯克尔,只要使用 :e file . 这将打开标准编辑器并允许您编辑一些文件。之后,使用 :r 重新加载它。它将自动重新编译。

请注意,在此之后,所有“特别”定义的函数都将丢失。有关更多信息,请参阅文档。

ghci 使用 haskeline 对于命令行输入历史记录,可以向上滚动以重复/编辑输入。您的输入历史记录通常记录在一个文件中,您可以找到 ghci_history 在给出的目录中

System.Directory.getAppUserDataDirectory "ghc"

有各种命令可以探索“context”(:show bindings、:show modules、:def、…),但它们的输出不足以重现您的会话(尽管仍然值得了解它们)。

一般来说,建议结合 GHCI 打开编辑器窗口的会话是健全的:如果它不仅仅是一次性定义,即使只是为了调试目的,最好将其包含在要加载到的模块中 GHCI ,以便您可以重用它。

哦,如果“context”,您的意思是要加载的一些默认设置或模块,在每个项目的基础上,还有 GHCI 的 configuration file . 也便于定义自己的 GHCI 命令。

在OCAML中,您可以构建自己的顶级。它至少解决了加载模块的问题。

http://caml.inria.fr/pub/docs/manual-ocaml/toplevel.html#sec278

ocamlmktop命令生成包含用户代码的ocaml toplevels 启动时预加载。

ocamlmktop命令将一组.cmo和.cma文件作为参数, 并将它们与实现OCAML的对象文件链接 托普维尔典型用途是:

    ocamlmktop -o mytoplevel foo.cmo bar.cmo gee.cmo

这将创建字节码文件mytoplevel,其中包含ocaml 顶级系统,加上三个.cmo文件中的代码。这个 TopLevel是直接可执行的,由以下人员启动:

    ./mytoplevel

这将进入一个常规的顶级循环,除了 foo.cmo、bar.cmo和gee.cmo已经加载到内存中,就像 你已经打字:

    #load "foo.cmo";;
    #load "bar.cmo";;
    #load "gee.cmo";;

在顶层入口。FOO、BAR和GEE模块不是 打开了,不过,你还是要做

    open Foo;;

你自己,如果这是你想要的。

这也一直困扰着我,所以我写了一个快速的python/expect script 在每次GHCI会议开始时重放GHCI历史记录。

它不是很光滑。例如,它总是重复整个历史,这可能很慢。