Skip to content

Commit

Permalink
chore: more unresolved dump-state output, do not resolve during overr…
Browse files Browse the repository at this point in the history 
…ide lookup (#143)

```
    "default": {
      "unresolved": {
        "Remote": {
          "origin": "leanprover/lean4-nightly",
          "release": "nightly",
          "from_channel": "nightly"
        }
      },
      "resolved": {
        "Ok": "leanprover/lean4-nightly:nightly-2024-11-23"
      }
    },
    "active_override": {
      "unresolved": {
        "Remote": {
          "origin": "leanprover/lean4",
          "release": "stable",
          "from_channel": "stable"
        }
      },
      "reason": "Environment"
    },
    "resolved_active": {
      "Ok": "leanprover/lean4:v4.13.0"
    }
```
  • Loading branch information
@Kha
Kha authored Nov 25, 2024
1 parent d7920ac commit 99413ca
Show file tree
Hide file tree
Showing 7 changed files with 128 additions and 104 deletions.
2 changes: 2 additions & 0 deletions Cargo.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

28 changes: 20 additions & 8 deletions src/elan-cli/json_dump.rs
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
use elan::{lookup_toolchain_desc_ext, utils::{self, fetch_latest_release_tag}, Cfg, Toolchain};
use elan::{lookup_unresolved_toolchain_desc, resolve_toolchain_desc, utils::{self, fetch_latest_release_tag}, Cfg, Toolchain, UnresolvedToolchainDesc};
use std::{io, path::PathBuf};

use serde_derive::Serialize;
Expand All @@ -25,18 +25,24 @@ struct InstalledToolchain {
#[derive(Serialize)]
struct DefaultToolchain {
/// Not necessarily resolved name as given to `elan default`, e.g. `stable`
unresolved: String,
unresolved: UnresolvedToolchainDesc,
/// Fully resolved name; `Err` if `unresolved` needed to be resolved but there was a network error
resolved: Result<String>,
}

#[derive(Serialize)]
struct Override {
unresolved: UnresolvedToolchainDesc,
reason: OverrideReason,
}

#[derive(Serialize)]
struct Toolchains {
installed: Vec<InstalledToolchain>,
/// `None` if no default toolchain configured
default: Option<DefaultToolchain>,
/// `None` if no override for current directory configured, in which case `default` if any is used
active_override: Option<OverrideReason>,
active_override: Option<Override>,
/// Toolchain, if any, ultimately chosen based on `default` and `active_override`
resolved_active: Option<Result<String>>,
}
Expand All @@ -52,7 +58,10 @@ impl StateDump {
let newest = fetch_latest_release_tag("leanprover/elan", None, no_net);
let ref cwd = utils::current_dir()?;
let active_override = cfg.find_override(cwd)?;
let default = cfg.get_default()?;
let default = match cfg.get_default()? {
None => None,
Some(d) => Some(lookup_unresolved_toolchain_desc(cfg, &d)?)
};
Ok(StateDump {
elan_version: Version {
current: env!("CARGO_PKG_VERSION").to_string(),
Expand All @@ -67,15 +76,18 @@ impl StateDump {
}).collect(),
default: default.as_ref().map(|default| DefaultToolchain {
unresolved: default.clone(),
resolved: lookup_toolchain_desc_ext(cfg, &default, no_net)
resolved: resolve_toolchain_desc(cfg, &default, no_net)
.map(|t| t.to_string())
.map_err(|e| e.to_string()),
}),
active_override: active_override.as_ref().map(|p| p.1.clone()),
active_override: active_override.as_ref().map(|(desc, reason)| Override {
unresolved: desc.clone(),
reason: reason.clone(),
}),
resolved_active: active_override
.map(|p| p.0.desc.to_string())
.map(|p| p.0)
.or(default)
.map(|t| lookup_toolchain_desc_ext(cfg, &t, no_net)
.map(|t| resolve_toolchain_desc(cfg, &t, no_net)
.map(|tc| tc.to_string())
.map_err(|e| e.to_string()))
},
Expand Down
2 changes: 2 additions & 0 deletions src/elan-dist/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@ json = "0.12.4"
zip = "0.6"
filetime = "0.2.14"
time = "0.3"
serde = "1.0.119"
serde_derive = "1.0.119"
fslock = "0.2.1"

[target."cfg(windows)".dependencies]
Expand Down
3 changes: 2 additions & 1 deletion src/elan-dist/src/dist.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,13 +4,14 @@ use errors::*;
use manifestation::Manifestation;
use prefix::InstallPrefix;
use regex::Regex;
use serde_derive::Serialize;

use std::{fmt, fs};

// Fully-resolved toolchain descriptors. These always have full target
// triples attached to them and are used for canonical identification,
// such as naming their installation directory.
#[derive(Debug, Clone, PartialEq)]
#[derive(Debug, Clone, PartialEq, Serialize)]
pub enum ToolchainDesc {
// A linked toolchain
Local {
Expand Down
2 changes: 2 additions & 0 deletions src/elan-dist/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,8 @@ extern crate json;
extern crate sha2;
extern crate time;
extern crate zip;
extern crate serde;
extern crate serde_derive;

#[cfg(not(windows))]
extern crate libc;
Expand Down
150 changes: 70 additions & 80 deletions src/elan/config.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ use toolchain::Toolchain;

use toml;

use crate::{gc, lookup_toolchain_desc, read_toolchain_desc_from_file};
use crate::{gc, lookup_toolchain_desc, lookup_unresolved_toolchain_desc, read_toolchain_desc_from_file, UnresolvedToolchainDesc};

#[derive(Debug, Serialize, Clone)]
pub enum OverrideReason {
Expand Down Expand Up @@ -148,87 +148,31 @@ impl Cfg {
}
}

pub fn find_override(&self, path: &Path) -> Result<Option<(Toolchain, OverrideReason)>> {
let mut override_ = None;

pub fn find_override(&self, path: &Path) -> Result<Option<(UnresolvedToolchainDesc, OverrideReason)>> {
// First check ELAN_TOOLCHAIN
if let Some(ref name) = self.env_override {
override_ = Some((
lookup_toolchain_desc(self, name)?,
return Ok(Some((
lookup_unresolved_toolchain_desc(self, name)?,
OverrideReason::Environment,
));
)));
}

// Then walk up the directory tree from 'path' looking for either the
// directory in override database, a `lean-toolchain` file, or a
// `leanpkg.toml` file.
if override_.is_none() {
self.settings_file.with(|s| {
override_ = self.find_override_from_dir_walk(path, s)?;

Ok(())
})?;
}

if let Some((name, reason)) = override_ {
// This is hackishly using the error chain to provide a bit of
// extra context about what went wrong. The CLI will display it
// on a line after the proximate error.

let reason_err = match reason {
OverrideReason::Environment => {
"the ELAN_TOOLCHAIN environment variable specifies an uninstalled toolchain"
.to_string()
}
OverrideReason::OverrideDB(ref path) => {
format!(
"the directory override for '{}' specifies an uninstalled toolchain",
path.display()
)
}
OverrideReason::ToolchainFile(ref path) => {
format!(
"the toolchain file at '{}' specifies an uninstalled toolchain",
path.display()
)
}
OverrideReason::LeanpkgFile(ref path) => {
format!(
"the leanpkg.toml file at '{}' specifies an uninstalled toolchain",
path.display()
)
}
OverrideReason::InToolchainDirectory(ref path) => {
format!(
"could not parse toolchain directory at '{}'",
path.display()
)
}
};

match self.get_toolchain(&name, false) {
Ok(toolchain) => {
if toolchain.exists() {
Ok(Some((toolchain, reason)))
} else {
toolchain.install_from_dist()?;
Ok(Some((toolchain, reason)))
}
}
Err(e) => Err(e)
.chain_err(|| Error::from(reason_err))
.chain_err(|| ErrorKind::OverrideToolchainNotInstalled(name)),
}
} else {
Ok(None)
if let Some(res) = self.settings_file.with(|s| {
self.find_override_from_dir_walk(path, s)
})? {
return Ok(Some(res));
}
Ok(None)
}

fn find_override_from_dir_walk(
&self,
dir: &Path,
settings: &Settings,
) -> Result<Option<(ToolchainDesc, OverrideReason)>> {
) -> Result<Option<(UnresolvedToolchainDesc, OverrideReason)>> {
let notify = self.notify_handler.as_ref();
let dir = utils::canonicalize_path(dir, &|n| notify(n.into()));
let mut dir = Some(&*dir);
Expand All @@ -237,15 +181,15 @@ impl Cfg {
// First check the override database
if let Some(name) = settings.dir_override(d, notify) {
let reason = OverrideReason::OverrideDB(d.to_owned());
return Ok(Some((name, reason)));
return Ok(Some((UnresolvedToolchainDesc(name), reason)));
}

// Then look for 'lean-toolchain'
let toolchain_file = d.join("lean-toolchain");
if let Ok(desc) = read_toolchain_desc_from_file(self, &toolchain_file) {
let reason = OverrideReason::ToolchainFile(toolchain_file);
gc::add_root(self, d)?;
return Ok(Some((desc, reason)));
return Ok(Some((UnresolvedToolchainDesc(desc), reason)));
}

// Then look for 'leanpkg.toml'
Expand All @@ -260,7 +204,7 @@ impl Cfg {
{
None => {}
Some(toml::Value::String(s)) => {
let desc = lookup_toolchain_desc(self, s)?;
let desc = lookup_unresolved_toolchain_desc(self, s)?;
return Ok(Some((desc, OverrideReason::LeanpkgFile(leanpkg_file))));
}
Some(a) => {
Expand All @@ -275,7 +219,7 @@ impl Cfg {
if let Some(last) = d.file_name() {
if let Some(last) = last.to_str() {
return Ok(Some((
ToolchainDesc::from_toolchain_dir(last)?,
UnresolvedToolchainDesc(ToolchainDesc::from_toolchain_dir(last)?),
OverrideReason::InToolchainDirectory(d.into()),
)));
}
Expand All @@ -290,15 +234,61 @@ impl Cfg {
&self,
path: &Path,
) -> Result<Option<(Toolchain, Option<OverrideReason>)>> {
Ok(
if let Some((toolchain, reason)) = self.find_override(path)? {
Some((toolchain, Some(reason)))
} else if let Some(tc) = self.resolve_default()? {
Some((self.get_toolchain(&tc, false)?, None))
} else {
None
},
)
if let Some((toolchain, reason)) = self.find_override(path)? {
match self.get_toolchain(&toolchain.0, false) {
Ok(toolchain) => {
if toolchain.exists() {
Ok(Some((toolchain, Some(reason))))
} else {
toolchain.install_from_dist()?;
Ok(Some((toolchain, Some(reason))))
}
}
Err(e) => {
// This is hackishly using the error chain to provide a bit of
// extra context about what went wrong. The CLI will display it
// on a line after the proximate error.

let reason_err = match reason {
OverrideReason::Environment => {
"the ELAN_TOOLCHAIN environment variable specifies an uninstalled toolchain"
.to_string()
}
OverrideReason::OverrideDB(ref path) => {
format!(
"the directory override for '{}' specifies an uninstalled toolchain",
path.display()
)
}
OverrideReason::ToolchainFile(ref path) => {
format!(
"the toolchain file at '{}' specifies an uninstalled toolchain",
path.display()
)
}
OverrideReason::LeanpkgFile(ref path) => {
format!(
"the leanpkg.toml file at '{}' specifies an uninstalled toolchain",
path.display()
)
}
OverrideReason::InToolchainDirectory(ref path) => {
format!(
"could not parse toolchain directory at '{}'",
path.display()
)
}
};
Err(e)
.chain_err(|| Error::from(reason_err))
.chain_err(|| ErrorKind::OverrideToolchainNotInstalled(toolchain.0))
}
}
} else if let Some(tc) = self.resolve_default()? {
Ok(Some((self.get_toolchain(&tc, false)?, None)))
} else {
Ok(None)
}
}

pub fn get_overrides(&self) -> Result<Vec<(String, ToolchainDesc)>> {
Expand Down
Loading

0 comments on commit 99413ca

Please sign in to comment.