agda_mode/agda/
verify.rs

1use std::io;
2use std::io::ErrorKind;
3
4use crate::agda::ReplState;
5use crate::cmd::Cmd;
6use crate::resp::DisplayInfo;
7
8pub fn check_version(version: &str) -> io::Result<()> {
9    // I don't expect earlier versions to have interaction-json :)
10    if version.starts_with("2.4") || version.starts_with("2.5") || version.starts_with("2.6.0") {
11        let msg = format!("Expected Agda 2.6.1 or higher, got: {}", version);
12        Err(io::Error::new(ErrorKind::InvalidData, msg))
13    } else {
14        Ok(())
15    }
16}
17
18impl ReplState {
19    pub async fn validate_version_panicking(&mut self) {
20        match self.validate_version().await {
21            Ok(()) => {}
22            Err(e) => panic!("{}", e.to_string()),
23        }
24    }
25
26    /// Validate this Agda repl.
27    pub async fn validate_version(&mut self) -> io::Result<()> {
28        self.command(Cmd::ShowVersion).await?;
29        let version = loop {
30            match self.next_display_info().await? {
31                DisplayInfo::Version { version } => break version,
32                _ => {}
33            }
34        };
35        // other checks?
36        check_version(&version)
37    }
38}
agda_mode/agda/verify.rs

agda_mode/agda/
verify.rs
