flams/
main.rs

1mod check;
2#[cfg(any(doc, feature = "docs"))]
3pub mod endpoints;
4
5use std::path::{Path, PathBuf};
6
7#[allow(unused_imports)]
8use flams_stex::STEX;
9use flams_system::settings::{BuildQueueSettings, ServerSettings, SettingsSpec};
10use ftml_uris::ArchiveId;
11
12fn in_tokio(f: impl Future<Output = ()>) {
13    let mut rt = tokio::runtime::Builder::new_multi_thread();
14    rt.enable_all();
15    rt.build()
16        .expect("Failed to initialize Tokio runtime")
17        .block_on(async move {
18            tokio::select! {
19            () = f => {},
20            _ = tokio::signal::ctrl_c() => std::process::exit(0)
21            }
22        });
23}
24fn in_tokio_fn(f: impl FnOnce() + Send + 'static) {
25    let mut rt = tokio::runtime::Builder::new_multi_thread();
26    rt.enable_all();
27    rt.build()
28        .expect("Failed to initialize Tokio runtime")
29        .block_on(async move {
30            tokio::select! {
31            r = tokio::task::spawn_blocking(f) => {
32                r.expect("this is a bug");
33            },
34            _ = tokio::signal::ctrl_c() => std::process::exit(0)
35            }
36        });
37}
38
39fn main() {
40    let mut cli = Cli::get();
41    match cli.command.take() {
42        Some(Commands::Build {
43            archive,
44            path,
45            persist,
46            verbose,
47        }) => {
48            let mut settings: SettingsSpec = cli.into();
49            settings.buildqueue.num_threads = Some(1);
50            in_tokio_fn(move || {
51                flams_system::settings::Settings::initialize(settings);
52                check::check(archive, path, persist, !verbose);
53            });
54        }
55        None => flams_main::main(cli.into()),
56    }
57}
58
59#[derive(clap::Parser, Debug)]
60#[command(name="flams",propagate_version = true, version, about, long_about = Some(
61"𝖥𝖫∀𝖬∫ - Flexiformal Annotation Management System\n\
62--------------------------------------------------------------------\n\
63See the \u{1b}]8;;https://github.com/UniFormal/MMT\u{1b}\\documentation\u{1b}]8;;\u{1b}\\ for details"
64))]
65pub struct Cli {
66    /// a comma-separated list of `MathHub` paths (if not given, the default paths are used
67    /// as determined by the MATHHUB system variable or ~/.mathhub/mathhub.path)
68    #[arg(short, long)]
69    pub(crate) mathhubs: Option<String>,
70
71    /// whether to enable debug logging
72    #[arg(short, long)]
73    pub(crate) debug: Option<bool>,
74
75    #[arg(short, long)]
76    /// The toml config file to use
77    pub(crate) config_file: Option<PathBuf>,
78
79    #[arg(short, long)]
80    /// The log directory to use
81    pub(crate) log_dir: Option<PathBuf>,
82
83    #[arg(long)]
84    /// The stack size in MB used for every thread
85    pub(crate) stack_size: Option<u8>,
86
87    #[arg(long)]
88    /// The directory used for temporary files
89    pub(crate) temp_dir: Option<PathBuf>,
90
91    #[arg(long)]
92    /// The directory used for embedding models for vector search
93    pub(crate) embedding_dir: Option<PathBuf>,
94
95    #[arg(short, long)]
96    /// The admin password to use for the server
97    pub(crate) admin_pwd: Option<String>,
98
99    /// Network port to use for the server
100    #[arg(long,value_parser = clap::value_parser!(u16).range(1..))]
101    pub(crate) port: Option<u16>,
102
103    /// Network address to use for the server
104    #[arg(long)]
105    pub(crate) ip: Option<String>,
106
107    #[arg(long)]
108    pub(crate) external_url: Option<String>,
109
110    #[arg(long)]
111    /// The database file to use for account management etc.
112    pub(crate) db: Option<PathBuf>,
113
114    #[arg(long)]
115    /// The directory to use for the rdf triple store.
116    pub(crate) rdf_database: Option<PathBuf>,
117
118    /// The number of threads to use for the buildqueue
119    #[arg(short, long)]
120    pub(crate) threads: Option<u8>,
121
122    /// enter lsp mode
123    #[arg(long)]
124    pub(crate) lsp: bool,
125
126    #[arg(long)]
127    pub(crate) gitlab_url: Option<String>,
128
129    #[arg(long)]
130    pub(crate) gitlab_token: Option<String>,
131    #[arg(long)]
132    pub(crate) gitlab_app_id: Option<String>,
133    #[arg(long)]
134    pub(crate) gitlab_app_secret: Option<String>,
135    #[arg(long)]
136    pub(crate) gitlab_redirect_url: Option<String>,
137    #[command(subcommand)]
138    command: Option<Commands>,
139}
140
141#[derive(clap::Subcommand, Debug)]
142enum Commands {
143    /// Checks a single file
144    Build {
145        /// The archive of the file
146        #[arg(short, long)]
147        archive: ArchiveId,
148        /// The file path relative to the archive's source directory
149        #[arg(short, long)]
150        path: PathBuf,
151        /// Whether to write the build to disk (otherwise, results are printed and discarded)
152        #[arg(long)]
153        persist: bool,
154        /// Print entire proof trees; otherwise, successful steps are not expanded
155        #[arg(long)]
156        verbose: bool,
157    },
158}
159
160#[allow(clippy::fallible_impl_from)]
161impl From<Cli> for SettingsSpec {
162    fn from(cli: Cli) -> Self {
163        fn from_file(cfg_file: &Path) -> SettingsSpec {
164            let cfg = std::fs::read_to_string(cfg_file).unwrap_or_else(|e| {
165                panic!("Could not read config file {}: {e}", cfg_file.display())
166            });
167            let cfg: SettingsSpec = toml::from_str(&cfg).unwrap_or_else(|e| {
168                panic!("Could not parse config file {}: {e}", cfg_file.display())
169            });
170            cfg
171        }
172        let (cfg, mut settings) = cli.into();
173        settings += SettingsSpec::from_envs();
174        if let Some(cfg_file) = cfg {
175            if cfg_file.exists() {
176                settings += from_file(&cfg_file);
177            } else {
178                panic!("Could not find config file {}", cfg_file.display());
179            }
180        } else if let Ok(path) = std::env::current_exe()
181            && let Some(path) = path.parent()
182        {
183            let path = path.join("settings.toml");
184            if path.exists() {
185                settings += from_file(&path);
186            }
187        }
188        settings
189    }
190}
191impl From<Cli> for (Option<PathBuf>, SettingsSpec) {
192    /// #### Panics
193    fn from(cli: Cli) -> Self {
194        let settings = SettingsSpec {
195            mathhubs: cli
196                .mathhubs
197                .map(|s| s.split(',').map(|s| PathBuf::from(s.trim())).collect())
198                .unwrap_or_default(),
199            debug: cli.debug,
200            stack_size: cli.stack_size,
201            database: cli.db.map(PathBuf::into_boxed_path),
202            rdf_database: cli.rdf_database.map(PathBuf::into_boxed_path),
203            log_dir: cli.log_dir.map(PathBuf::into_boxed_path),
204            temp_dir: cli.temp_dir.map(PathBuf::into_boxed_path),
205            embedding_dir: cli.embedding_dir.map(PathBuf::into_boxed_path),
206            server: ServerSettings {
207                port: cli.port.unwrap_or_default(),
208                ip: cli.ip.map(|s| s.parse().expect("Illegal ip")),
209                admin_pwd: cli.admin_pwd,
210                external_url: cli.external_url,
211            },
212            buildqueue: BuildQueueSettings {
213                num_threads: cli.threads,
214            },
215            gitlab: flams_utils::settings::GitlabSettings {
216                url: cli.gitlab_url.map(|s| s.parse().expect("Illegal url")),
217                token: cli.gitlab_token.map(Into::into),
218                app_id: cli.gitlab_app_id.map(Into::into),
219                app_secret: cli.gitlab_app_secret.map(Into::into),
220                redirect_url: cli.gitlab_redirect_url.map(Into::into),
221            },
222            lsp: cli.lsp,
223            remotes: std::collections::HashMap::default(),
224            fonts: std::collections::HashMap::default(),
225        };
226        (cli.config_file, settings)
227    }
228}
229
230impl Cli {
231    #[must_use]
232    #[inline]
233    fn get() -> Self {
234        use clap::Parser;
235        Self::parse()
236    }
237}
flams/main.rs

flams/
main.rs
