Change Verus source to asterinas\verus (#3)

* A little more robust

* Remove patch-apply

* Change verus source

Author: rikosellic

src/main.rs

@@ -99,6 +99,12 @@ struct BootstrapArgs {
         action = ArgAction::SetTrue
     )]
     debug: bool,
+
+    #[arg(long = "test_branch", 
+        help = "Use the test branch of our Verus fork for testing",
+        default_value = "false", 
+        action = ArgAction::SetTrue)]
+    test_branch: bool,
 }
 
 #[derive(Parser, Debug)]
@@ -396,6 +402,11 @@ fn bootstrap(args: &BootstrapArgs) -> Result<(), DynError> {
     let options = verus::install::VerusInstallOpts {
         release: !args.debug,
         restart: args.restart,
+        branch: if args.test_branch {
+            Some("update-test".into())
+        } else {
+            None
+        },
     };
 
     if args.upgrade {

src/verus.rs

@@ -139,8 +139,7 @@ pub fn get_target_dir() -> PathBuf {
 
 #[memoize]
 pub fn get_verus_target_dir() -> PathBuf {
-    let root = get_root();
-    let verus_dir = root.join("tools").join("verus");
+    let verus_dir = install::verus_dir();
     verus_dir
         .join("source")
         .join("target-verus")
@@ -1007,8 +1006,7 @@ pub fn exec_verify(
         }
 
         if options.count_line {
-            let root = get_root();
-            let verus_root = root.join("tools").join("verus");
+            let verus_root = install::verus_dir();
             let line_count_dir = verus_root.join("source/tools/line_count");
             let dependency_file = env::current_dir()?.join("lib.d");
             env::set_current_dir(&line_count_dir)?;
@@ -1098,9 +1096,10 @@ pub mod install {
     pub struct VerusInstallOpts {
         pub restart: bool,
         pub release: bool,
+        pub branch: Option<String>,
     }
 
-    pub const VERUS_REPO: &str = "https://github.com/verus-lang/verus.git";
+    pub const VERUS_REPO: &str = "https://github.com/asterinas/verus.git";
 
     #[memoize]
     pub fn tools_dir() -> PathBuf {
@@ -1122,11 +1121,6 @@ pub mod install {
         tools_dir().join("patches")
     }
 
-    #[memoize]
-    pub fn verus_analyzer_dir() -> PathBuf {
-        tools_dir().join("verus-analyzer")
-    }
-
     pub fn clone_repo(verus_dir: &Path) -> Result<(), DynError> {
         info!(
             "Cloning Verus repo {} to {} ...",
@@ -1260,6 +1254,10 @@ pub mod install {
     pub fn exec_bootstrap(options: &VerusInstallOpts) -> Result<(), DynError> {
         let verus_dir = verus_dir();
 
+        if options.branch.is_some() {
+            error!("Specifying a branch is only supported during upgrade.");
+        }
+
         if options.restart && verus_dir.exists() {
             info!("Removing old verus installation...");
             std::fs::remove_dir_all(&verus_dir)?;
@@ -1274,15 +1272,15 @@ pub mod install {
         install_z3()?;
 
         // Apply patches
-        let verus_patch = tools_patch_dir().join("verus-fixes.patch");
+        /*let verus_patch = tools_patch_dir().join("verus-fixes.patch");
         if verus_patch.exists() && !commands::is_patch_applied(&verus_dir, &verus_patch) {
             status!(
                 "Applying patch {} to {} ...",
                 verus_patch.display(),
                 verus_dir.display()
             );
             commands::apply_patch(&verus_dir, &verus_patch);
-        }
+        }*/
 
         // Build Verus
         build_verus(options.release)?;
@@ -1302,7 +1300,7 @@ pub mod install {
         Ok(())
     }
 
-    pub fn git_pull(dir: &Path) -> Result<(), DynError> {
+    pub fn git_pull(dir: &Path, branch: Option<&str>) -> Result<(), DynError> {
         let repo = Repository::open(dir).unwrap_or_else(|e| {
             error!(
                 "Unable to find the git repo of verus under {}: {}",
@@ -1311,9 +1309,12 @@ pub mod install {
             );
         });
 
-        // Find the remote and fetch all branches
+        // Determine target branch (default to "main")
+        let target_branch = branch.unwrap_or("main");
+
+        // Find the remote and fetch the target branch
         let mut remote = repo.find_remote("origin")?;
-        remote.fetch(&["main"], None, None)?; // Fetch all branches
+        remote.fetch(&[target_branch], None, None)?;
 
         // Get the current branch
         let head = repo.head()?;
@@ -1325,7 +1326,7 @@ pub mod install {
         let local_commit = head.peel_to_commit()?;
 
         // Find the matching remote branch
-        let upstream_branch = format!("refs/remotes/origin/{}", branch_name);
+        let upstream_branch = format!("refs/remotes/origin/{}", target_branch);
         let upstream_ref = repo.find_reference(&upstream_branch)?;
         let upstream_commit = upstream_ref.peel_to_commit()?;
 
@@ -1337,7 +1338,18 @@ pub mod install {
             status!("Already up to date");
         } else if analysis.is_fast_forward() {
             // Fast-forward
-            let refname = format!("refs/heads/{}", branch_name);
+            let refname = format!("refs/heads/{}", target_branch);
+
+            // Create local branch if it doesn't exist
+            if repo.find_reference(&refname).is_err() {
+                repo.reference(
+                    &refname,
+                    upstream_commit.id(),
+                    false,
+                    &format!("Create branch {}", target_branch),
+                )?;
+            }
+
             let mut reference = repo.find_reference(&refname)?;
             reference.set_target(upstream_commit.id(), "Fast-forward")?;
             repo.set_head(&refname)?;
@@ -1347,7 +1359,11 @@ pub mod install {
             checkout_opts.force();
             repo.checkout_head(Some(&mut checkout_opts))?;
 
-            status!("Fast-forwarded {} to {}", branch_name, upstream_commit.id());
+            status!(
+                "Fast-forwarded {} to {}",
+                target_branch,
+                upstream_commit.id()
+            );
         } else {
             // Need to perform a merge
             let mut merge_opts = git2::MergeOptions::new();
@@ -1374,15 +1390,15 @@ pub mod install {
                 Some("HEAD"),
                 &sig,
                 &sig,
-                &format!("Merge remote-tracking branch 'origin/{}'", branch_name),
+                &format!("Merge remote-tracking branch 'origin/{}'", target_branch),
                 &tree,
                 &[&local_commit, &upstream_commit],
             )?;
 
             // Clean up merge state
             repo.cleanup_state()?;
 
-            status!("Merged origin/{} into {}", branch_name, branch_name);
+            status!("Merged origin/{} into {}", target_branch, target_branch);
         }
 
         status!(
@@ -1401,7 +1417,7 @@ pub mod install {
 
         // git pull the Verus repo
         let verus_dir = verus_dir();
-        git_pull(&verus_dir)?;
+        git_pull(&verus_dir, options.branch.as_ref().map(|s| s.as_str()))?;
         status!("Verus repo updated to the latest version");
 
         // Build Verus