isabelle_client/client/
results.rs

1/// Contains the result data types the Isabelle servers responses with
2use serde::{Deserialize, Serialize};
3
4/// Describes a source position within Isabelle text
5#[derive(Deserialize, Serialize, Debug)]
6struct Position {
7    line: Option<usize>,
8    offset: Option<usize>,
9    end_offset: Option<usize>,
10    filed: Option<String>,
11    id: Option<usize>,
12}
13
14#[derive(Deserialize, Serialize, Debug)]
15pub struct Message {
16    /// The main message kinds are writeln (for regular output), warning, error.
17    kind: String,
18    message: String,
19    pos: Option<Position>,
20}
21
22#[derive(Deserialize, Serialize, Debug)]
23pub struct TheoryProgress {
24    /// = "writeln"
25    kind: String,
26    message: String,
27    session: String,
28    percentage: Option<usize>,
29}
30
31#[derive(Deserialize, Serialize, Debug)]
32pub struct Timing {
33    elapsed: f64,
34    cpu: f64,
35    gc: f64,
36}
37
38#[derive(Serialize, Deserialize, Debug)]
39pub struct Task {
40    task: String,
41}
42
43#[derive(Deserialize, Serialize, Debug)]
44pub struct Node {
45    node_name: String,
46    theory_name: String,
47}
48
49#[derive(Deserialize, Serialize, Debug)]
50pub struct NodeStatus {
51    ok: bool,
52    total: usize,
53    unprocessed: usize,
54    running: usize,
55    warned: usize,
56    failed: usize,
57    canceled: bool,
58    consolidated: bool,
59    percentage: usize,
60}
61
62#[derive(Deserialize, Serialize, Debug)]
63pub struct NodesStatus {
64    status: Vec<(Node, NodeStatus)>,
65}
66
67#[derive(Deserialize, Serialize, Debug)]
68pub struct Export {
69    name: String,
70    base64: bool,
71    body: String,
72}
73
74/// Results per sessions for `session_build` command
75#[derive(Deserialize, Serialize, Debug)]
76pub struct SessionBuildResult {
77    /// The target session name as specified by the command
78    pub session: String,
79    /// True if building was successful
80    pub ok: bool,
81    /// Is zero if `ok` is true. Non-zero return code indicates and error.
82    pub return_code: usize,
83    /// If true, the build process was aborted after running too long
84    timeout: bool,
85    /// Overall timing
86    timing: Timing,
87}
88
89/// Results for `session_build` command
90#[derive(Deserialize, Serialize, Debug)]
91pub struct SessionBuildResults {
92    /// All sessions ok
93    pub ok: bool,
94    /// Is zero if `ok` is true. Non-zero return code indicates and error.
95    return_code: usize,
96    /// The result of each build sessions
97    pub sessions: Vec<SessionBuildResult>,
98}
99
100/// Results for `session_start` command
101#[derive(Deserialize, Serialize, Debug)]
102pub struct SessionStartResult {
103    pub task: String,
104    /// Internal identification of the session object within the server process
105    pub session_id: String,
106    /// Temporary directory that is specifically cre- ated for this session and deleted after it has been stopped.
107    /// As tmp_dir is the default master_dir for commands use_theories and purge_theories, theory files copied there may be used without further path specification.
108    pub tmp_dir: Option<String>,
109}
110
111/// Results for `session_stop` command
112#[derive(Deserialize, Serialize, Debug)]
113pub struct SessionStopResult {
114    pub task: String,
115    pub ok: bool,
116    pub return_code: usize,
117}
118
119/// Result per node as returned from the `use_theories` command
120#[derive(Deserialize, Serialize, Debug)]
121pub struct NodeResults {
122    #[serde(flatten)]
123    node: Node,
124    status: NodeStatus,
125    messages: Vec<Message>,
126    exports: Vec<Export>,
127}
128
129/// Results for `use_theories` command
130#[derive(Deserialize, Serialize, Debug)]
131pub struct UseTheoryResults {
132    pub task: String,
133    pub ok: bool,
134    pub errors: Vec<Message>,
135    pub nodes: Vec<NodeResults>,
136}
137
138#[derive(Deserialize, Serialize, Debug, Default)]
139pub struct PurgedTheory {
140    pub node_name: String,
141    pub theory_name: String,
142}
143
144/// Results for `purge_theories` command.
145///
146/// The system manual states that the result is of the form `{purged: [String]}`, which is incorrect.
147/// The struct models what is actually returned by the server.
148#[derive(Deserialize, Serialize, Debug, Default)]
149pub struct PurgeTheoryResults {
150    pub purged: Vec<PurgedTheory>,
151    pub retained: Vec<PurgedTheory>,
152}
isabelle_client/client/results.rs

isabelle_client/client/
results.rs
