Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

lean: init elan #124

Merged
merged 1 commit into from
Sep 29, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/lean.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
pub mod elan;
9 changes: 9 additions & 0 deletions src/lean/elan.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
use structopt::StructOpt;

#[derive(Debug, StructOpt)]
pub struct ElanConfig {
#[structopt(long, default_value = "3")]
pub retain_elan_versions: usize,
#[structopt(long, default_value = "30")]
pub retain_lean_versions: usize,
}
33 changes: 32 additions & 1 deletion src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ mod html_scanner;
mod index_pipe;
#[macro_use]
mod merge_pipe;
mod lean;
mod metadata;
mod opts;
mod pypi;
Expand Down Expand Up @@ -226,7 +227,7 @@ fn main() {
let script_src = rewrite_pipe::RewritePipe::new(
stream_pipe::ByteStreamPipe::new(
source.get_script(),
buffer_path.clone().unwrap(),
buffer_path.clone().expect("buffer path is not present"),
false,
),
buffer_path.clone().unwrap(),
Expand Down Expand Up @@ -321,6 +322,36 @@ fn main() {
index_bytes_pipe!(buffer_path, prefix, false, 999)
);
}
Source::Elan(source) => {
let elan_src = stream_pipe::ByteStreamPipe::new(
GitHubRelease::new(
String::from("leanprover/elan"),
source.retain_elan_versions,
),
buffer_path.clone().unwrap(),
true,
);
let lean_src = stream_pipe::ByteStreamPipe::new(
GitHubRelease::new(
String::from("leanprover/lean4"),
source.retain_lean_versions,
),
buffer_path.clone().unwrap(),
true,
);
let unified = merge_pipe! {
elan: elan_src,
lean: lean_src,
};
let indexed = index_pipe::IndexPipe::new(
unified,
buffer_path.clone().unwrap(),
prefix.clone().unwrap(),
999,
);

transfer!(opts, indexed, transfer_config, id_pipe!());
}
}
});
}
3 changes: 3 additions & 0 deletions src/opts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ use crate::ghcup::Ghcup as GhcupConfig;
use crate::github_release::GitHubRelease;
use crate::gradle::Gradle;
use crate::homebrew::HomebrewConfig;
use crate::lean::elan::ElanConfig;
use crate::pypi::Pypi as PypiConfig;
use crate::rsync::Rsync as RsyncConfig;
use crate::rustup::Rustup as RustupConfig;
Expand Down Expand Up @@ -37,6 +38,8 @@ pub enum Source {
Gradle(Gradle),
#[structopt(about = "rustup")]
Rustup(RustupConfig),
#[structopt(about = "elan")]
Elan(ElanConfig),
}

#[derive(Debug)]
Expand Down
2 changes: 1 addition & 1 deletion src/pypi.rs
Original file line number Diff line number Diff line change
Expand Up @@ -193,7 +193,7 @@ async fn bigquery_index(logger: &Logger) -> Result<Vec<String>> {

fn version_from_filename(filename: &str) -> Option<Version> {
static RE_VERSION: once_cell::sync::Lazy<Regex> = once_cell::sync::Lazy::new(|| {
Regex::new(r#"^\w+-([\w.-_+]+).*(.tar.gz|tar.bz2|.zip|.whl|.exe|.egg)$"#).unwrap()
Regex::new(r"^\w+-([\w.-_+]+).*(.tar.gz|tar.bz2|.zip|.whl|.exe|.egg)$").unwrap()
});
RE_VERSION
.captures(filename)
Expand Down
Loading