Remove vpl and fix compilation issues on Ubuntu

Author: zhengyao-lin

Makefile

@@ -1,5 +1,5 @@
 # In topological order of dependencies
-PROJECTS = vest polyfill parser vpl chain test
+PROJECTS = chain parser polyfill rspec_test test vest
 
 .PHONY: debug
 debug:

chain/Makefile

@@ -17,16 +17,16 @@ DOMAINS = github.com google.com outlook.com slack.com verus.rs
 .PHONY: test-policy-%
 test-policy-%: target/debug/chain
 # For each domain in DOMAINS, remove the suffix, then find the corresponding pem
-	@for domain in $(DOMAINS); do \
+	@set -e; \
+	for domain in $(DOMAINS); do \
 		pem_file=tests/chains/$${domain%%.*}.pem; \
 		printf "[$*] $$domain: "; \
 		echo "target/debug/chain $*-hammurabi tests/roots.pem $$pem_file $$domain -t $(TEST_TIME) -s"; \
-		(target/debug/chain \
+		target/debug/chain \
 			$*-hammurabi \
 			tests/roots.pem \
 			$$pem_file \
 			$$domain \
 			-t $(TEST_TIME) \
-			-s) \
-		|| (echo "failed"; exit 1); \
+			-s; \
 	done

dep.mk

@@ -36,16 +36,17 @@ rust-deps-%: $(foreach dep,$(CARGO_DEPS),force-target/%/lib$(dep).rlib)
 # Bulid each dependency in VERUS_DEPS
 .PHONY: verus-deps-%
 verus-deps-%:
-	@for dep in $(VERUS_DEPS); do \
-		pushd ../$$dep; \
+	@set -e; \
+	for dep in $(VERUS_DEPS); do \
+		cd ../$$dep; \
 		echo "Building Verus dependency $$dep"; \
 		rlib=target/$*/lib$$dep.rlib; \
-		make $$rlib || (echo "Fail to compile dependency $$dep"; exit 1) && \
+		make $$rlib; \
 		if [ ! -f $$rlib ] || [ ! -f $$rlib.verusdata ]; then \
 			echo "Cannot find external Verus library $$rlib (or $$rlib.verusdata)"; \
 			exit 1; \
-		fi && \
-		popd; \
+		fi; \
+		cd -; \
     done
 
 # The main verus command to run for TARGET
@@ -61,7 +62,10 @@ VERUS_COMMAND = \
 		--crate-name $(NAME) \
 		$(if $(filter %.rlib,$@),--crate-type=lib,) \
 		-L dependency=target/$*/deps \
-		$(foreach dep,$(CARGO_DEPS),--extern $(subst -,_,$(dep))=$(firstword $(wildcard target/$*/deps/lib$(subst -,_,$(dep))-*.rlib) $(wildcard target/$*/deps/lib$(dep)-*.dylib))) \
+		$(foreach dep,$(CARGO_DEPS),--extern $(subst -,_,$(dep))=$(firstword \
+			$(wildcard target/$*/deps/lib$(subst -,_,$(dep))-*.rlib) \
+			$(wildcard target/$*/deps/lib$(subst -,_,$(dep))-*.so) \
+			$(wildcard target/$*/deps/lib$(subst -,_,$(dep))-*.dylib))) \
 		$(foreach dep,$(VERUS_DEPS),-L dependency=../$(dep)/target/$*/deps) \
 		$(foreach dep,$(VERUS_DEPS),-L dependency=../$(dep)/target/$*) \
 		$(foreach dep,$(VERUS_DEPS),--extern $(dep)=../$(dep)/target/$*/lib$(dep).rlib --import $(dep)=../$(dep)/target/$*/lib$(dep).rlib.verusdata) \

macros/Cargo.lock

@@ -17,7 +17,6 @@ mod default;
 mod eq;
 mod unreachable;
 mod cached;
-mod base64;
 
 pub use depend::*;
 pub use repeat::*;
@@ -34,7 +33,6 @@ pub use default::*;
 pub use eq::*;
 pub use unreachable::*;
 pub use cached::*;
-pub use base64::*;
 
 pub use macros::View;
 pub use macros::PolyfillClone;

parser/src/common/mod.rs

@@ -0,0 +1,2 @@
+[toolchain]
+channel = "1.76.0"

rust-toolchain.toml

@@ -1,6 +1,5 @@
 #![crate_name = "vest"]
 #![crate_type = "lib"]
-#![warn(missing_docs)]
 //! Vest is a *formally verified* library for parsing and serializing binary data, using combinators.
 //!
 //! # Background