稍后保存我的运行顶层 [英] Saving my running toplevel for later

问题描述

当在 ocaml 或 ghci toplevels中工作时，我经常为缺少一个对象而建立一个重要的上下文更好的单词，绑定的值，函数，加载的模块等等。有没有办法保存所有这些，并在以后重新加载，这样我就可以继续我刚刚离开的地方了？或者更好的是，将整个批次转储为一个文本文件，可以重新加载或修改为可以编译为可执行文件的代码（例如，通过添加一个Main）？

When working in the ocaml or ghci toplevels I often build up a significant "context" for want of a better word, values bound, functions, modules loaded, and so on. Is there a way to save all of that and reload it later so I can continue exactly where I left off? Or better yet, dump out the entire lot as a text file that could be reloaded or be trivially modified into code that I could compile into an executable (e.g. by adding a Main)?

推荐答案

HOL灯的使用者有有类似的需求，他们使用检查点程序来保存顶层的快照。请参阅caml邮件列表上的此消息，或 HOL教程的第8页。

Users of HOL light have had similar needs, and they use a checkpointing program to save a snapshot of the toplevel. See this message on the caml mailing-list, or page 8 of this HOL tutorial.

通常，最好将定义保留为源代码，而不是二进制顶层快照。许多工具允许将.ml文件快速加载到顶层以便于实验（emacs模式等）。请参阅HOL教程中的警告：

In general it is better to keep the definitions as source code, rather than a binary toplevel snapshot. Numerous tools allow to quickly load a .ml file into the toplevel for easy experimentation (emacs modes, etc.). See the warning in the HOL tutorial:

在HOL中开发大型校样时，应始终将校样脚本保存为
an OCaml文件准备重新加载，而不是依靠ckpt。这将允许稍后修改证据
，供其他人使用。但是，制作
中间快照可以非常方便，因此您无需加载大型文件即可进一步处理证据。
这与编程中的常见情况类似：您应始终保留您的
完整源代码，但不要在每次使用
代码时重新编译所有源代码。

When developing large proofs in HOL, you should always keep the proof script as an OCaml file ready to reload, rather than relying on ckpt. This will allow the proofs to be later modified, used by others etc. However, it can be very convenient to make intermediate snapshots so you do not have to load large files to work further on a proof. This is analogous to the usual situation in programming: you should always keep your complete source code, but don’t want to recompile all the sources each time you use the code.

这篇关于稍后保存我的运行顶层的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！