以下是一个示例

use isabelle_client::client::{AsyncResult, IsabelleClient, SyncResult};
use isabelle_client::client::args::*;
use isabelle_client::server::run_server;
use tokio_test::block_on;

// Start a server and connect to it
let mut server = run_server(Some("test-server")).unwrap();
let mut client = IsabelleClient::for_server(&server);

// Start session HOL
let session_args = SessionBuildArgs::session("HOL");
let session = block_on(client.session_start(&session_args)).unwrap();
// Load `Drinker` theory into the HOL session
let th_args = UseTheoriesArgs::for_session(&session.finished().session_id, &["~~/src/HOL/Examples/Drinker"]);
let load_th = block_on(client.use_theories(&th_args)).unwrap();
// Assert loading theory was successful
assert!(load_th.finished().ok);

// Exit the server 
server.exit();

服务器

使用 run_server 函数启动 Isabelle 服务器或获取已知名称的本地运行实例的凭据（端口、密码）。可以使用 exit 方法退出正在运行的服务器。

以下是一个启动名为 "my-server" 的服务器的示例。

use isabelle_client::server::run_server;

// Run an Isabelle server named "my-server" locally
let mut server = run_server(Some("my-server")).unwrap();

// ...

// Exit the server
server.exit();

请注意，这只是一个对 isabelle server -n my-server 的包装器。特别是，如果本地已运行名为 "my-server" 的服务器，则函数将返回现有服务器的端口和密码。

批量模式

batch_process 函数是对异步调用 isabelle process 工具的包装。它接受一个 ProcessArgs 参数，该参数由以下内容组成：

• 要加载的理论
• 会话目录
• 可选的逻辑会话名称，以及
• 选项，以键值对的形式给出

可用的选项可以在系统手册中找到或使用 isabelle options 命令。 OptionsBuilder 提供了一种方便的方式来构建常见选项。

以下是一个示例

use isabelle_client::process::{batch_process, ProcessArgs};
use tokio_test::block_on;

let args = ProcessArgs::load_theories(&[String::from("~~/src/HOL/Examples/Drinker")]);
let output = block_on(batch_process(&args, None));
assert!(output.unwrap().status.success());

许可证

此库根据 MIT 许可证授权。有关详细信息，请参阅 LICENSE 文件。