Dashboard: Use custom stages feature (rust-lang#582)

* Upgrade litani to latest version

* Use custom stages. Other minor fixes.

Author: adpaco-aws

scripts/ci/update_dashboard.py

@@ -44,7 +44,8 @@ def main():
         run = BeautifulSoup(fp, 'html.parser')
 
     # Update pipeline names to link to the example under test
-    for row in run.find_all('div', attrs={'class': 'pipeline-row'}):
+    for row in run.find_all(lambda tag: tag.name == 'div' and
+                                   tag.get('class') == ['pipeline-row']):
         path = row.find('div', attrs={'class': 'pipeline-name'})
         # Some paths here may be `None` - skip them
         if path.p:

src/tools/dashboard/src/books.rs

@@ -421,8 +421,11 @@ fn litani_run_tests() {
     let output_prefix: PathBuf = ["build", "output"].iter().collect();
     let output_symlink: PathBuf = output_prefix.join("latest");
     let dashboard_dir: PathBuf = ["src", "test", "dashboard"].iter().collect();
+    let stage_names = ["check", "codegen", "verification"];
+
     util::add_rmc_and_litani_to_path();
-    let mut litani = Litani::init("RMC", &output_prefix, &output_symlink);
+    let mut litani = Litani::init("RMC", &stage_names, &output_prefix, &output_symlink);
+
     // Run all tests under the `src/test/dashboard` directory.
     for entry in WalkDir::new(dashboard_dir) {
         let entry = entry.unwrap().into_path();

src/tools/dashboard/src/litani.rs

@@ -152,7 +152,12 @@ pub struct Litani {
 
 impl Litani {
     /// Sets up a new [`Litani`] run.
-    pub fn init(project_name: &str, output_prefix: &Path, output_symlink: &Path) -> Self {
+    pub fn init(
+        project_name: &str,
+        stage_names: &[&str],
+        output_prefix: &Path,
+        output_symlink: &Path,
+    ) -> Self {
         Command::new("litani")
             .args([
                 "init",
@@ -162,7 +167,9 @@ impl Litani {
                 output_prefix.to_str().unwrap(),
                 "--output-symlink",
                 output_symlink.to_str().unwrap(),
+                "--stages",
             ])
+            .args(stage_names)
             .spawn()
             .unwrap()
             .wait()
@@ -231,6 +238,11 @@ impl Litani {
         }
         self.spawned_commands.clear();
         // Run `run-build` command and wait for it to finish.
-        Command::new("litani").arg("run-build").spawn().unwrap().wait().unwrap();
+        Command::new("litani")
+            .args(["run-build", "--no-pipeline-dep-graph"])
+            .spawn()
+            .unwrap()
+            .wait()
+            .unwrap();
     }
 }

src/tools/dashboard/src/main.rs

@@ -1,6 +1,5 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-#![feature(command_access)]
 #![feature(extend_one)]
 #![feature(rustc_private)]
 

src/tools/dashboard/src/util.rs

@@ -163,8 +163,7 @@ pub fn add_check_job(litani: &mut Litani, test_props: &TestProps) {
     let exit_status = if test_props.fail_step == Some(FailStep::Check) { 1 } else { 0 };
     let mut rmc_rustc = Command::new("rmc-rustc");
     rmc_rustc.args(&test_props.rustc_args).args(["-Z", "no-codegen"]).arg(&test_props.path);
-    // TODO: replace `build` with `check` when Litani adds support for custom
-    // stages (see https://github.com/model-checking/rmc/issues/391).
+
     let mut phony_out = test_props.path.clone();
     phony_out.set_extension("check");
     litani.add_job(
@@ -173,7 +172,7 @@ pub fn add_check_job(litani: &mut Litani, test_props: &TestProps) {
         &[&phony_out],
         "Is this valid Rust code?",
         test_props.path.to_str().unwrap(),
-        "build",
+        "check",
         exit_status,
         5,
     );
@@ -188,6 +187,8 @@ pub fn add_codegen_job(litani: &mut Litani, test_props: &TestProps) {
         .args([
             "-Z",
             "codegen-backend=gotoc",
+            "-Z",
+            "trim-diagnostic-paths=no",
             "--cfg=rmc",
             "--out-dir",
             "build/tmp",
@@ -196,8 +197,7 @@ pub fn add_codegen_job(litani: &mut Litani, test_props: &TestProps) {
             "--crate-type=lib",
         ])
         .arg(&test_props.path);
-    // TODO: replace `test` with `codegen` when Litani adds support for custom
-    // stages (see https://github.com/model-checking/rmc/issues/391).
+
     let mut phony_in = test_props.path.clone();
     phony_in.set_extension("check");
     let mut phony_out = test_props.path.clone();
@@ -208,7 +208,7 @@ pub fn add_codegen_job(litani: &mut Litani, test_props: &TestProps) {
         &[&phony_out],
         "Does RMC support all the Rust features used in it?",
         test_props.path.to_str().unwrap(),
-        "test",
+        "codegen",
         exit_status,
         5,
     );
@@ -222,8 +222,7 @@ pub fn add_verification_job(litani: &mut Litani, test_props: &TestProps) {
     if !test_props.rustc_args.is_empty() {
         rmc.env("RUSTFLAGS", test_props.rustc_args.join(" "));
     }
-    // TODO: replace `report` with `verification` when Litani adds support for
-    // custom stages (see https://github.com/model-checking/rmc/issues/391).
+
     let mut phony_in = test_props.path.clone();
     phony_in.set_extension("codegen");
     litani.add_job(
@@ -232,7 +231,7 @@ pub fn add_verification_job(litani: &mut Litani, test_props: &TestProps) {
         &[],
         "Can RMC reason about it?",
         test_props.path.to_str().unwrap(),
-        "report",
+        "verification",
         exit_status,
         10,
     );