diff --git a/.github/BUILD.md b/.github/BUILD.md index 027d4f1bf..5b1007ea1 100644 --- a/.github/BUILD.md +++ b/.github/BUILD.md @@ -39,31 +39,77 @@ Release publication is controlled by [.github/release-config.env](./release-conf - `PVS_RELEASE_DEV_BRANCH` - `PVS_RELEASE_VERSION` -Those variables determine which branches feed the stable/dev release tracks and which PVS version is embedded in branch-created release tags. +Those variables determine the stable branch used to validate official release +tags, the branch that feeds the rolling development prerelease, and the PVS +version embedded in release tags. The current release policy is: -- pushes to the configured stable branch publish or update a release tagged `pvs8.1-master-YYYYMMDD` -- pushes to the configured dev branch publish or update a prerelease tagged `pvs8.1-dev-YYYYMMDD` -- pushes of git tags whose commits are contained in the configured stable branch publish stable releases using the pushed tag name +- pushes to the configured dev branch publish or update the rolling prerelease tagged `pvs8.1-dev` +- pushes to the configured stable branch do not publish a release by themselves +- pushing a sequential tag such as `pvs8.1.1`, `pvs8.1.2`, or `pvs8.1.3` publishes a stable release when the tagged commit is contained in the configured stable branch +- stable releases are explicitly marked as the latest GitHub Release +- tag names outside the configured `pvs.` series are rejected by the release policy - the `publish-release` job in [.github/workflows/release-builds.yml](./workflows/release-builds.yml) is the only job that mutates GitHub Releases - the GitHub Releases page publishes the standalone platform tarballs for successful builds; macOS notarized `.pkg` assets are published in addition to those tarballs when signing and notarization are enabled - each stable or dev asset family is reconciled once in that final publish job, so the release keeps only the latest asset for each platform/package kind -This keeps stable and dev builds on the same GitHub Releases page while still letting the branch mapping be changed in one place during branch-based testing. +The normal promotion sequence is to merge `dev` into `master`, create the next +`pvs8.1.N` tag on that master commit, and push the tag. Development then +continues on `dev`, whose moving `pvs8.1-dev` prerelease is updated by the next +successful dev build. + +For example, after the release merge is present on `master`: + +```sh +git switch master +git pull --ff-only origin master +git tag -a pvs8.1.1 -m "PVS 8.1.1" +git push origin pvs8.1.1 +git switch dev +``` ## Which Artifact To Distribute If the goal is to minimize Gatekeeper friction for end users, distribute the notarized `.pkg` artifact when one is available. The standalone platform tarballs are also published on the GitHub Releases page for successful builds. -Build artifacts and GitHub Release assets use the same naming scheme: `pvs----.tgz` for standalone tarballs and `pvs----.pkg` for notarized macOS packages. The current release flow vendors any non-system dylib dependencies discovered in the packaged runtime directory so the shipped bundle does not reach back into Homebrew on an end user's machine. The `.pkg` path then signs those Mach-O payload files, signs the installer package, and notarizes that packaged distribution. +Internal GitHub Actions artifacts remain date-stamped as +`pvs----.tgz` or `.pkg` so concurrent CI runs cannot +collide. The final GitHub Release assets use stable names: + +- `pvs-linux-x86_64.tgz` +- `pvs-linux-aarch64.tgz` +- `pvs-macos-arm64.tgz` +- `pvs-macos-x86_64.tgz` +- `pvs-macos-arm64.pkg`, when signing and notarization are enabled +- `pvs-macos-x86_64.pkg`, when signing and notarization are enabled + +The current release flow vendors any non-system dylib dependencies discovered +in the packaged runtime directory so the shipped bundle does not reach back +into Homebrew on an end user's machine. The `.pkg` path then signs those Mach-O +payload files, signs the installer package, and notarizes that packaged +distribution. + +The stable names provide durable download URLs. For example: + +- latest official Linux x86_64: `https://github.com/SRI-CSL/PVS/releases/latest/download/pvs-linux-x86_64.tgz` +- rolling dev Linux x86_64: `https://github.com/SRI-CSL/PVS/releases/download/pvs8.1-dev/pvs-linux-x86_64.tgz` + +Every build writes an ignored `metadata.json` at the source-tree root. Release +bundles contain their own `metadata.json` with the PVS version and target, +UTC build time, Git and commit details, GitHub Actions provenance when +available, toolchain versions, and a SHA-256 manifest of the packaged PVS +native binaries, Lisp cores, dynamic libraries, and ASDF system definitions. +Documentation, examples, headers, and solver input files are not inventoried. +Release auditing requires valid metadata. macOS installer packaging refreshes +the manifest after payload signing so its hashes describe the bytes shipped in +the `.pkg`. ## Release Tracks -- Stable branch releases are named with the PVS version, branch, and UTC date, for example `pvs8.1-master-20260420`. -- Stable version-tag releases are still supported when the pushed tag's commit is on the configured stable branch. -- Dev releases are prereleases named with the PVS version, branch, and UTC date, for example `pvs8.1-dev-20260420`. -- If multiple stable or dev builds run on the same UTC date, they update the same release for that channel and replace its assets in place. +- Stable releases use explicit, permanent tags in the `pvs8.1.N` series, and the tagged commit must be contained in `master`. +- Dev builds update the single moving prerelease tag `pvs8.1-dev` and replace its assets in place. +- The UTC build date remains in internal Actions artifact filenames; published GitHub Release assets use stable names. - Asset cleanup is centralized in the final publish job so old Linux/macOS tarballs and notarized macOS packages are pruned in one pass instead of by the individual builders. For the SBCL runtime, the packaged bundle now uses: @@ -210,20 +256,20 @@ base64 < ~/cert/AuthKey_.p8 | tr -d '\n' ## Setting Secrets With `gh` -Examples below use `karthiknukala/PVS`. Replace that if you are configuring a different repository. +Examples below use `SRI-CSL/PVS`. Replace that if you are configuring a different repository. ```bash -base64 < ~/cert/DeveloperIDApplication.p12 | tr -d '\n' | gh secret set MACOS_DEV_ID_APPLICATION_CERT_P12_BASE64 -R karthiknukala/PVS -gh secret set MACOS_DEV_ID_APPLICATION_CERT_PASSWORD -R karthiknukala/PVS -gh secret set MACOS_DEV_ID_APPLICATION_CERT_NAME -R karthiknukala/PVS --body "Developer ID Application: Your Name (TEAMID)" +base64 < ~/cert/DeveloperIDApplication.p12 | tr -d '\n' | gh secret set MACOS_DEV_ID_APPLICATION_CERT_P12_BASE64 -R SRI-CSL/PVS +gh secret set MACOS_DEV_ID_APPLICATION_CERT_PASSWORD -R SRI-CSL/PVS +gh secret set MACOS_DEV_ID_APPLICATION_CERT_NAME -R SRI-CSL/PVS --body "Developer ID Application: Your Name (TEAMID)" -base64 < ~/cert/Certificates.p12 | tr -d '\n' | gh secret set MACOS_DEV_ID_INSTALLER_CERT_P12_BASE64 -R karthiknukala/PVS -gh secret set MACOS_DEV_ID_INSTALLER_CERT_PASSWORD -R karthiknukala/PVS -gh secret set MACOS_DEV_ID_INSTALLER_CERT_NAME -R karthiknukala/PVS --body "Developer ID Installer: Your Name (TEAMID)" +base64 < ~/cert/Certificates.p12 | tr -d '\n' | gh secret set MACOS_DEV_ID_INSTALLER_CERT_P12_BASE64 -R SRI-CSL/PVS +gh secret set MACOS_DEV_ID_INSTALLER_CERT_PASSWORD -R SRI-CSLPVS +gh secret set MACOS_DEV_ID_INSTALLER_CERT_NAME -R SRI-CSL/PVS --body "Developer ID Installer: Your Name (TEAMID)" -gh secret set MACOS_NOTARY_ISSUER_ID -R karthiknukala/PVS -gh secret set MACOS_NOTARY_KEY_ID -R karthiknukala/PVS -base64 < ~/cert/AuthKey_.p8 | tr -d '\n' | gh secret set MACOS_NOTARY_API_KEY_P8_BASE64 -R karthiknukala/PVS +gh secret set MACOS_NOTARY_ISSUER_ID -R SRI-CSL/PVS +gh secret set MACOS_NOTARY_KEY_ID -R SRI-CSL/PVS +base64 < ~/cert/AuthKey_.p8 | tr -d '\n' | gh secret set MACOS_NOTARY_API_KEY_P8_BASE64 -R SRI-CSL/PVS ``` ## What Happens Once All Secrets Are Set @@ -256,7 +302,7 @@ It does not currently use the alternate Apple ID + app-specific password flow fo If the pkg job is skipped: - Check that all nine secrets are present. -- `gh secret list -R karthiknukala/PVS` will show secret names, but not values. +- `gh secret list -R SRI-CSL/PVS` will show secret names, but not values. If the `Developer ID Application` or `Developer ID Installer` identity does not appear after importing the `.cer`: diff --git a/.github/scripts/audit-release-artifact.sh b/.github/scripts/audit-release-artifact.sh index 54c88b7dd..2e6d12409 100755 --- a/.github/scripts/audit-release-artifact.sh +++ b/.github/scripts/audit-release-artifact.sh @@ -6,9 +6,10 @@ usage() { cat <<'EOF' Usage: audit-release-artifact.sh --artifact FILE [--path PATH ...] [--foreign-build-root PATH ...] -Extracts a release archive and fails if any forbidden build-machine path appears -in the payload. If --path is omitted, paths are read from -PVS_RELEASE_FORBIDDEN_PATHS, one per line. +Extracts a release archive, validates its metadata.json and SHA-256 artifact +manifest, and fails if any forbidden build-machine path appears in the payload. +If --path is omitted, paths are read from PVS_RELEASE_FORBIDDEN_PATHS, one per +line. If --foreign-build-root is provided, only absolute references to the PVS runtime foreign libraries under that root are rejected. This catches SBCL saved @@ -78,6 +79,17 @@ case $artifact in ;; esac +metadata_generator="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd -P)/generate-build-metadata.py" +[[ -f $metadata_generator ]] || fail "metadata validator not found: $metadata_generator" +metadata_files=() +while IFS= read -r -d '' metadata_file; do + metadata_files+=("$metadata_file") +done < <(find "$tmpdir" -type f -name metadata.json -print0) +[[ ${#metadata_files[@]} -eq 1 ]] || fail "release artifact must contain exactly one metadata.json; found ${#metadata_files[@]}" +python3 "$metadata_generator" \ + --validate "${metadata_files[0]}" \ + --verify-artifacts "$(dirname "${metadata_files[0]}")" + clean=true matches_file="$tmpdir/matches" for forbidden_path in "${paths[@]}"; do diff --git a/.github/scripts/build-macos-pkg.sh b/.github/scripts/build-macos-pkg.sh index b5246ed1c..4ceec6d08 100755 --- a/.github/scripts/build-macos-pkg.sh +++ b/.github/scripts/build-macos-pkg.sh @@ -171,18 +171,37 @@ cp -R "$bundle_dir" "$stage_root$install_base/" bundle_macos_runtime_deps "$stage_root$install_base/$(basename "$bundle_dir")" +staged_bundle="$stage_root$install_base/$(basename "$bundle_dir")" +metadata_generator="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd -P)/generate-build-metadata.py" +metadata_file="$staged_bundle/metadata.json" +[[ -f $metadata_generator ]] || fail "metadata generator not found: $metadata_generator" +[[ -f $metadata_file ]] || fail "bundle metadata not found: $metadata_file" + if [[ -n ${MACOS_APPLICATION_SIGN_IDENTITY:-} ]]; then echo "Signing staged Mach-O payload with $MACOS_APPLICATION_SIGN_IDENTITY" if [[ -n $application_sign_entitlements ]]; then [[ -f $application_sign_entitlements ]] || fail "MACOS_APPLICATION_SIGN_ENTITLEMENTS_FILE does not exist: $application_sign_entitlements" fi sign_macho_payload \ - "$stage_root$install_base/$(basename "$bundle_dir")" \ + "$staged_bundle" \ "$MACOS_APPLICATION_SIGN_IDENTITY" \ "$signing_keychain" \ "$application_sign_entitlements" fi +# Payload signing changes Mach-O bytes, so refresh the embedded manifest before +# pkgbuild seals the installer payload. +python3 "$metadata_generator" \ + --refresh "$metadata_file" \ + --artifact-root "$staged_bundle" \ + --artifact pvs.asd \ + --artifact bin \ + --artifact yices \ + --packaging-format macos-pkg +python3 "$metadata_generator" \ + --validate "$metadata_file" \ + --verify-artifacts "$staged_bundle" + pkg_stem=${pkg_name%.pkg} unsigned_pkg="$output_dir/$pkg_stem-unsigned.pkg" signed_pkg="$output_dir/$pkg_name" diff --git a/.github/scripts/generate-build-metadata.py b/.github/scripts/generate-build-metadata.py new file mode 100644 index 000000000..186fd1a9a --- /dev/null +++ b/.github/scripts/generate-build-metadata.py @@ -0,0 +1,518 @@ +#!/usr/bin/env python3 +"""Generate and validate provenance metadata for PVS builds.""" + +import argparse +import datetime as dt +import hashlib +import json +import os +import platform +import re +import subprocess +import sys +import tempfile +import urllib.parse +from pathlib import Path + + +SCHEMA_VERSION = 1 +SHA256_RE = re.compile(r"^[0-9a-f]{64}$") +DYNAMIC_LIBRARY_RE = re.compile(r"(?:\.dylib$|\.so(?:\.|$))") +NATIVE_BINARY_MAGICS = ( + b"\x7fELF", + b"\xfe\xed\xfa\xce", + b"\xfe\xed\xfa\xcf", + b"\xce\xfa\xed\xfe", + b"\xcf\xfa\xed\xfe", + b"\xca\xfe\xba\xbe", + b"\xbe\xba\xfe\xca", + b"\xca\xfe\xba\xbf", + b"\xbf\xba\xfe\xca", + b"MZ", +) + + +def utc_now(): + return dt.datetime.now(dt.timezone.utc).replace(microsecond=0) + + +def iso_utc(value): + return value.isoformat().replace("+00:00", "Z") + + +def run(command, cwd=None): + try: + result = subprocess.run( + command, + cwd=str(cwd) if cwd else None, + check=False, + stdout=subprocess.PIPE, + stderr=subprocess.DEVNULL, + text=True, + ) + except OSError: + return None + if result.returncode != 0: + return None + return result.stdout.strip() + + +def first_line(command, cwd=None): + output = run(command, cwd=cwd) + return output.splitlines()[0] if output else None + + +def git_value(source_root, *arguments): + return run(["git", "-C", str(source_root), *arguments]) + + +def sanitize_remote(remote): + if not remote: + return None + if remote.startswith("git@") and ":" in remote: + return remote + parsed = urllib.parse.urlsplit(remote) + if parsed.scheme not in ("http", "https", "ssh", "git") or not parsed.hostname: + return None + username = "git@" if parsed.scheme == "ssh" and parsed.username == "git" else "" + port = ":{}".format(parsed.port) if parsed.port else "" + return urllib.parse.urlunsplit( + (parsed.scheme, "{}{}{}".format(username, parsed.hostname, port), parsed.path, "", "") + ) + + +def git_metadata(source_root): + head = git_value(source_root, "rev-parse", "HEAD") + if not head: + return {"available": False} + + status = git_value(source_root, "status", "--porcelain=v1", "--untracked-files=all") or "" + status_lines = status.splitlines() + tracked_changes = sum(1 for line in status_lines if not line.startswith("??")) + untracked_files = sum(1 for line in status_lines if line.startswith("??")) + branch = git_value(source_root, "symbolic-ref", "--quiet", "--short", "HEAD") + tags_text = git_value(source_root, "tag", "--points-at", "HEAD") or "" + parents_text = git_value(source_root, "show", "-s", "--format=%P", "HEAD") or "" + + commit = { + "sha": head, + "short_sha": git_value(source_root, "rev-parse", "--short=12", "HEAD"), + "tree_sha": git_value(source_root, "show", "-s", "--format=%T", "HEAD"), + "parent_shas": parents_text.split() if parents_text else [], + "subject": git_value(source_root, "show", "-s", "--format=%s", "HEAD"), + "author": { + "name": git_value(source_root, "show", "-s", "--format=%an", "HEAD"), + "email": git_value(source_root, "show", "-s", "--format=%ae", "HEAD"), + "date": git_value(source_root, "show", "-s", "--format=%aI", "HEAD"), + }, + "committer": { + "name": git_value(source_root, "show", "-s", "--format=%cn", "HEAD"), + "email": git_value(source_root, "show", "-s", "--format=%ce", "HEAD"), + "date": git_value(source_root, "show", "-s", "--format=%cI", "HEAD"), + }, + "signature": { + "status": git_value(source_root, "show", "-s", "--format=%G?", "HEAD"), + "signer": git_value(source_root, "show", "-s", "--format=%GS", "HEAD") or None, + "key": git_value(source_root, "show", "-s", "--format=%GK", "HEAD") or None, + }, + } + + return { + "available": True, + "version": first_line(["git", "--version"]), + "branch": branch, + "detached": branch is None, + "describe": git_value(source_root, "describe", "--tags", "--always", "--dirty"), + "tags_at_commit": sorted(tags_text.splitlines()), + "is_shallow": git_value(source_root, "rev-parse", "--is-shallow-repository") == "true", + "is_dirty": bool(status_lines), + "tracked_changes": tracked_changes, + "untracked_files": untracked_files, + "remote": sanitize_remote(git_value(source_root, "config", "--get", "remote.origin.url")), + "commit": commit, + } + + +def github_metadata(): + if os.environ.get("GITHUB_ACTIONS") != "true": + return None + server = os.environ.get("GITHUB_SERVER_URL", "https://github.com") + repository = os.environ.get("GITHUB_REPOSITORY") + run_id = os.environ.get("GITHUB_RUN_ID") + run_url = None + if repository and run_id: + run_url = "{}/{}/actions/runs/{}".format(server.rstrip("/"), repository, run_id) + return { + "provider": "github-actions", + "repository": repository, + "repository_url": "{}/{}".format(server.rstrip("/"), repository) if repository else None, + "workflow": os.environ.get("GITHUB_WORKFLOW"), + "workflow_ref": os.environ.get("GITHUB_WORKFLOW_REF"), + "workflow_sha": os.environ.get("GITHUB_WORKFLOW_SHA"), + "run_id": run_id, + "run_number": os.environ.get("GITHUB_RUN_NUMBER"), + "run_attempt": os.environ.get("GITHUB_RUN_ATTEMPT"), + "run_url": run_url, + "job": os.environ.get("GITHUB_JOB"), + "event": os.environ.get("GITHUB_EVENT_NAME"), + "actor": os.environ.get("GITHUB_ACTOR"), + "ref": os.environ.get("GITHUB_REF"), + "ref_name": os.environ.get("GITHUB_REF_NAME"), + "ref_type": os.environ.get("GITHUB_REF_TYPE"), + "head_ref": os.environ.get("GITHUB_HEAD_REF") or None, + "base_ref": os.environ.get("GITHUB_BASE_REF") or None, + "sha": os.environ.get("GITHUB_SHA"), + "runner_os": os.environ.get("RUNNER_OS"), + "runner_arch": os.environ.get("RUNNER_ARCH"), + } + + +def parse_platform(pvs_platform): + architecture, separator, operating_system = pvs_platform.partition("-") + return { + "pvs_platform": pvs_platform, + "architecture": architecture if separator else platform.machine(), + "operating_system": operating_system if separator else platform.system(), + } + + +def parse_toolchains(values): + toolchains = { + "python": platform.python_version(), + "git": first_line(["git", "--version"]), + "make": first_line(["make", "--version"]), + "c_compiler": first_line([os.environ.get("CC", "cc"), "--version"]), + } + for value in values: + name, separator, version = value.partition("=") + if separator and name and version: + toolchains[name] = version + return {key: value for key, value in toolchains.items() if value} + + +def sha256_file(path): + digest = hashlib.sha256() + with path.open("rb") as stream: + for block in iter(lambda: stream.read(1024 * 1024), b""): + digest.update(block) + return digest.hexdigest() + + +def artifact_entry(path, artifact_root, component): + relative_path = path.relative_to(artifact_root).as_posix() + stat_result = path.lstat() + entry = { + "path": relative_path, + "component": component, + "mode": "{:04o}".format(stat_result.st_mode & 0o7777), + "size_bytes": stat_result.st_size, + } + if path.is_symlink(): + entry.update({"type": "symlink", "target": os.readlink(str(path))}) + elif path.is_file(): + entry.update({"type": "file", "sha256": sha256_file(path)}) + else: + entry["type"] = "other" + return entry + + +def is_native_binary(path): + try: + with path.open("rb") as stream: + prefix = stream.read(4) + except OSError: + return False + return any(prefix.startswith(magic) for magic in NATIVE_BINARY_MAGICS) + + +def is_manifest_artifact(path, artifact_root, allow_asdf=False): + inspected_path = path + if path.is_symlink(): + try: + inspected_path = path.resolve(strict=True) + inspected_path.relative_to(artifact_root.resolve()) + except (OSError, ValueError): + return False + if not inspected_path.is_file(): + return False + name = inspected_path.name + return ( + (allow_asdf and name.endswith(".asd")) + or name.endswith(".core") + or DYNAMIC_LIBRARY_RE.search(name) is not None + or is_native_binary(inspected_path) + ) + + +def artifact_paths(candidate, artifact_root): + if candidate.is_symlink() or candidate.is_file(): + if is_manifest_artifact(candidate, artifact_root, allow_asdf=True): + yield candidate + return + if not candidate.is_dir(): + return + for directory, dirnames, filenames in os.walk(str(candidate), followlinks=False): + directory_path = Path(directory) + for dirname in list(dirnames): + path = directory_path / dirname + if path.is_symlink(): + if is_manifest_artifact(path, artifact_root): + yield path + dirnames.remove(dirname) + for filename in filenames: + path = directory_path / filename + if is_manifest_artifact(path, artifact_root): + yield path + + +def artifact_manifest(artifact_root, candidates, generated_at): + artifact_root = Path(os.path.abspath(str(artifact_root))) + entries_by_path = {} + for value in candidates: + candidate = Path(value) + if not candidate.is_absolute(): + candidate = artifact_root / candidate + candidate = Path(os.path.abspath(str(candidate))) + try: + component = candidate.relative_to(artifact_root).as_posix() + except ValueError: + raise ValueError("artifact is outside the artifact root: {}".format(value)) + for path in artifact_paths(candidate, artifact_root): + entry = artifact_entry(path, artifact_root, component) + entries_by_path[entry["path"]] = entry + return { + "generated_at": generated_at, + "hash_algorithm": "sha256", + "selection": [ + "native-binary", + "dynamic-library", + "lisp-core", + "asdf-system-definition", + ], + "components": sorted(set(candidates)), + "entries": [entries_by_path[path] for path in sorted(entries_by_path)], + } + + +def source_uri(git, github): + if github and github.get("repository_url"): + return github["repository_url"] + ".git" + return git.get("remote") if git.get("available") else None + + +def provenance(git, github): + commit_sha = git.get("commit", {}).get("sha") if git.get("available") else None + builder_id = "local" + if github: + builder_id = github.get("run_url") or github.get("workflow_ref") or "github-actions" + return { + "builder": {"id": builder_id}, + "source": { + "type": "git", + "uri": source_uri(git, github), + "digest": {"sha1": commit_sha} if commit_sha else None, + "ref": github.get("ref") if github else git.get("branch"), + }, + } + + +def source_date_metadata(): + raw_value = os.environ.get("SOURCE_DATE_EPOCH") + if not raw_value: + return None + try: + epoch = int(raw_value) + timestamp = iso_utc(dt.datetime.fromtimestamp(epoch, tz=dt.timezone.utc)) + except (ValueError, OverflowError, OSError): + return {"value": raw_value, "valid": False} + return {"value": epoch, "timestamp": timestamp, "valid": True} + + +def write_json(path, data): + path = Path(path) + path.parent.mkdir(parents=True, exist_ok=True) + descriptor, temporary_name = tempfile.mkstemp(prefix=path.name + ".", dir=str(path.parent)) + try: + with os.fdopen(descriptor, "w", encoding="utf-8") as stream: + json.dump(data, stream, indent=2, sort_keys=True) + stream.write("\n") + os.chmod(temporary_name, 0o644) + os.replace(temporary_name, str(path)) + except BaseException: + try: + os.unlink(temporary_name) + except OSError: + pass + raise + + +def validate(data): + if not isinstance(data, dict): + return ["metadata document must be a JSON object"] + errors = [] + if data.get("schema_version") != SCHEMA_VERSION: + errors.append("schema_version must be {}".format(SCHEMA_VERSION)) + for key in ("project", "build", "git", "provenance", "artifacts"): + if not isinstance(data.get(key), dict): + errors.append("{} must be an object".format(key)) + project = data.get("project", {}) if isinstance(data.get("project"), dict) else {} + if not project.get("name") or not project.get("version"): + errors.append("project name and version are required") + git = data.get("git", {}) if isinstance(data.get("git"), dict) else {} + commit = git.get("commit", {}) if isinstance(git.get("commit"), dict) else {} + if git.get("available") and not commit.get("sha"): + errors.append("git.commit.sha is required when git metadata is available") + artifacts = data.get("artifacts", {}) if isinstance(data.get("artifacts"), dict) else {} + components = artifacts.get("components") + if not isinstance(components, list) or not components: + errors.append("artifacts.components must be a non-empty array") + elif any(not isinstance(component, str) or not component for component in components): + errors.append("every artifact component must be a non-empty string") + entries = artifacts.get("entries") + if not isinstance(entries, list) or not entries: + errors.append("artifacts.entries must be a non-empty array") + else: + seen = set() + for index, entry in enumerate(entries): + path = entry.get("path") if isinstance(entry, dict) else None + if not isinstance(path, str) or not path: + errors.append("artifact {} has no path".format(index)) + continue + if path in seen: + errors.append("duplicate artifact path: {}".format(path)) + seen.add(path) + if entry.get("type") == "file": + digest = entry.get("sha256") + if not isinstance(digest, str) or not SHA256_RE.match(digest): + errors.append("artifact {} has an invalid SHA-256 digest".format(path)) + return errors + + +def verify_artifacts(data, artifact_root): + artifacts = data["artifacts"] + actual = artifact_manifest(artifact_root, artifacts["components"], artifacts["generated_at"]) + expected_entries = artifacts["entries"] + actual_by_path = {entry["path"]: entry for entry in actual["entries"]} + expected_by_path = {entry["path"]: entry for entry in expected_entries} + errors = [] + for path in sorted(set(expected_by_path) - set(actual_by_path)): + errors.append("manifest artifact is missing: {}".format(path)) + for path in sorted(set(actual_by_path) - set(expected_by_path)): + errors.append("artifact is absent from the manifest: {}".format(path)) + for path in sorted(set(expected_by_path) & set(actual_by_path)): + if expected_by_path[path] != actual_by_path[path]: + errors.append("artifact does not match the manifest: {}".format(path)) + return errors + + +def build_metadata(args): + now = utc_now() + generated_at = iso_utc(now) + source_root = Path(args.source_root).resolve() + github = github_metadata() + git = git_metadata(source_root) + build_id = "{}-{}".format( + git.get("commit", {}).get("short_sha") or "unknown", int(now.timestamp()) + ) + if github and github.get("run_id"): + build_id = "github-{}-{}-{}".format( + github["run_id"], github.get("run_attempt") or "1", github.get("job") or "job" + ) + return { + "schema_version": SCHEMA_VERSION, + "project": {"name": args.package, "version": args.version}, + "build": { + "id": build_id, + "generated_at": generated_at, + "generated_at_epoch_seconds": int(now.timestamp()), + "source_date_epoch": source_date_metadata(), + "target": parse_platform(args.platform), + "host": { + "operating_system": platform.system(), + "release": platform.release(), + "architecture": platform.machine(), + }, + "toolchains": parse_toolchains(args.toolchain), + }, + "git": git, + "ci": github, + "provenance": provenance(git, github), + "artifacts": artifact_manifest(args.artifact_root, args.artifact, generated_at), + } + + +def refresh_metadata(args): + metadata_path = Path(args.refresh) + with metadata_path.open(encoding="utf-8") as stream: + data = json.load(stream) + errors = validate(data) + if errors: + raise ValueError("cannot refresh invalid metadata: {}".format("; ".join(errors))) + generated_at = iso_utc(utc_now()) + data["artifacts"] = artifact_manifest(args.artifact_root, args.artifact, generated_at) + data.setdefault("packaging", []).append( + { + "format": args.packaging_format, + "payload_manifest_refreshed_at": generated_at, + "ci": github_metadata(), + } + ) + write_json(metadata_path, data) + + +def parse_arguments(): + parser = argparse.ArgumentParser(description=__doc__) + mode = parser.add_mutually_exclusive_group(required=True) + mode.add_argument("--output", help="write newly generated metadata to this path") + mode.add_argument("--refresh", help="refresh artifact hashes in an existing metadata file") + mode.add_argument("--validate", help="validate an existing metadata file") + parser.add_argument("--source-root", default=".") + parser.add_argument("--artifact-root", default=".") + parser.add_argument("--artifact", action="append", default=[]) + parser.add_argument("--package", default="pvs") + parser.add_argument("--version", default="unknown") + parser.add_argument("--platform", default=platform.machine() + "-" + platform.system()) + parser.add_argument("--toolchain", action="append", default=[]) + parser.add_argument("--packaging-format", default="unspecified") + parser.add_argument( + "--verify-artifacts", + help="with --validate, verify the manifest against this artifact root", + ) + return parser.parse_args() + + +def main(): + args = parse_arguments() + try: + if args.validate: + with Path(args.validate).open(encoding="utf-8") as stream: + data = json.load(stream) + errors = validate(data) + if not errors and args.verify_artifacts: + errors.extend(verify_artifacts(data, args.verify_artifacts)) + if errors: + for error in errors: + print("error: {}".format(error), file=sys.stderr) + return 1 + print("Valid PVS build metadata: {}".format(args.validate)) + return 0 + if not args.artifact: + raise ValueError("at least one --artifact is required") + if args.refresh: + refresh_metadata(args) + print("Refreshed PVS artifact metadata: {}".format(args.refresh)) + else: + data = build_metadata(args) + errors = validate(data) + if errors: + raise ValueError("generated invalid metadata: {}".format("; ".join(errors))) + write_json(args.output, data) + print("Generated PVS build metadata: {}".format(args.output)) + return 0 + except (OSError, ValueError, json.JSONDecodeError) as error: + print("error: {}".format(error), file=sys.stderr) + return 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/.github/scripts/prepare-release-build-tree.sh b/.github/scripts/prepare-release-build-tree.sh index d668aced0..a30429506 100755 --- a/.github/scripts/prepare-release-build-tree.sh +++ b/.github/scripts/prepare-release-build-tree.sh @@ -56,7 +56,7 @@ echo "Cloning release source $source_sha to $source_tree" git clone --no-local --quiet "$repo_dir" "$source_tree" git -C "$source_tree" checkout --quiet --detach "$source_sha" -for required in configure Makefile.in .github/scripts/audit-release-artifact.sh .github/scripts/strip-runtime-debug-info.sh; do +for required in configure Makefile.in .github/scripts/audit-release-artifact.sh .github/scripts/generate-build-metadata.py .github/scripts/strip-runtime-debug-info.sh; do [[ -e $source_tree/$required ]] || fail "prepared source tree is missing $required" done diff --git a/.github/scripts/publish-github-release.sh b/.github/scripts/publish-github-release.sh index 174c27051..20bcf6500 100644 --- a/.github/scripts/publish-github-release.sh +++ b/.github/scripts/publish-github-release.sh @@ -15,6 +15,7 @@ Usage: publish-github-release.sh \ [--target ] \ [--repo ] \ [--prerelease] \ + [--latest] \ [--move-tag] Publishes or updates a GitHub Release and uploads a single asset with a stable @@ -37,6 +38,7 @@ notes= target= repo=${GITHUB_REPOSITORY:-} prerelease=false +latest=false move_tag=false upload_asset= upload_tmpdir= @@ -83,6 +85,10 @@ while [[ $# -gt 0 ]]; do prerelease=true shift ;; + --latest) + latest=true + shift + ;; --move-tag) move_tag=true shift @@ -202,6 +208,9 @@ release_flags=(--title "$title" --notes-file "$notes_file") if [[ $prerelease == true ]]; then release_flags+=(--prerelease) fi +if [[ $latest == true ]]; then + release_flags+=(--latest) +fi if gh release view "$tag" -R "$repo" >/dev/null 2>&1; then gh release edit "$tag" -R "$repo" "${release_flags[@]}" diff --git a/.github/scripts/resolve-release-policy.sh b/.github/scripts/resolve-release-policy.sh index 5915a42a4..cb0675248 100644 --- a/.github/scripts/resolve-release-policy.sh +++ b/.github/scripts/resolve-release-policy.sh @@ -65,38 +65,39 @@ prerelease=false move_tag=false release_date=$(date -u +%Y%m%d) artifact_branch=$(sanitize_component "$GITHUB_REF_NAME") +release_version_pattern=${release_version//./\\.} +stable_tag_pattern="^pvs${release_version_pattern}\\.[1-9][0-9]*$" case ${GITHUB_REF_TYPE} in branch) - if [[ ${GITHUB_REF_NAME} == "$stable_branch" ]]; then - publish=true - channel=stable - release_tag="pvs${release_version}-${artifact_branch}-${release_date}" - release_title="PVS ${release_version} ${artifact_branch} ${release_date}" - prerelease=false - move_tag=true - elif [[ ${GITHUB_REF_NAME} == "$dev_branch" ]]; then + if [[ ${GITHUB_REF_NAME} == "$dev_branch" ]]; then publish=true channel=dev - release_tag="pvs${release_version}-${artifact_branch}-${release_date}" - release_title="PVS ${release_version} ${artifact_branch} ${release_date}" + release_tag="pvs${release_version}-${artifact_branch}" + release_title="PVS ${release_version} Development Snapshot" prerelease=true move_tag=true fi ;; tag) - git fetch --no-tags --depth=1 origin \ - "refs/heads/${stable_branch}:refs/remotes/origin/${stable_branch}" >/dev/null 2>&1 || { - fail "unable to fetch stable branch origin/${stable_branch} for tag validation" - } - if git merge-base --is-ancestor "$GITHUB_SHA" "refs/remotes/origin/${stable_branch}"; then - publish=true - channel=stable - release_tag=${GITHUB_REF_NAME} - release_title=${GITHUB_REF_NAME} - prerelease=false - move_tag=false - artifact_branch=$(sanitize_component "$stable_branch") + if [[ ${GITHUB_REF_NAME} =~ $stable_tag_pattern ]]; then + fetch_args=(--no-tags) + if [[ $(git rev-parse --is-shallow-repository 2>/dev/null) == true ]]; then + fetch_args+=(--unshallow) + fi + git fetch "${fetch_args[@]}" origin \ + "refs/heads/${stable_branch}:refs/remotes/origin/${stable_branch}" >/dev/null 2>&1 || { + fail "unable to fetch stable branch origin/${stable_branch} for tag validation" + } + if git merge-base --is-ancestor "$GITHUB_SHA" "refs/remotes/origin/${stable_branch}"; then + publish=true + channel=stable + release_tag=${GITHUB_REF_NAME} + release_title="PVS ${GITHUB_REF_NAME#pvs}" + prerelease=false + move_tag=false + artifact_branch=$(sanitize_component "$stable_branch") + fi fi ;; esac diff --git a/.github/workflows/release-builds.yml b/.github/workflows/release-builds.yml index 72dd79ee4..97cb81f1b 100644 --- a/.github/workflows/release-builds.yml +++ b/.github/workflows/release-builds.yml @@ -3,10 +3,9 @@ name: Release Builds on: push: branches: - - master - dev tags: - - '*' + - 'pvs8.1.*' workflow_dispatch: permissions: @@ -41,6 +40,7 @@ jobs: linux-x86: name: Linux x86 build needs: release-policy + if: ${{ needs.release-policy.outputs.publish == 'true' }} uses: ./.github/workflows/linux-x86-build.yml with: artifact_branch: ${{ needs.release-policy.outputs.artifact_branch }} @@ -49,6 +49,7 @@ jobs: linux-arm: name: Linux ARM build needs: release-policy + if: ${{ needs.release-policy.outputs.publish == 'true' }} uses: ./.github/workflows/linux-arm-build.yml with: artifact_branch: ${{ needs.release-policy.outputs.artifact_branch }} @@ -57,6 +58,7 @@ jobs: macos-arm: name: macOS arm64 build needs: release-policy + if: ${{ needs.release-policy.outputs.publish == 'true' }} uses: ./.github/workflows/apple-silicon-build.yml with: artifact_branch: ${{ needs.release-policy.outputs.artifact_branch }} @@ -66,6 +68,7 @@ jobs: macos-x86: name: macOS x86_64 build needs: release-policy + if: ${{ needs.release-policy.outputs.publish == 'true' }} uses: ./.github/workflows/apple-x86-build.yml with: artifact_branch: ${{ needs.release-policy.outputs.artifact_branch }} @@ -91,6 +94,7 @@ jobs: GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} RELEASE_ARTIFACT_BRANCH: ${{ needs.release-policy.outputs.artifact_branch }} RELEASE_ARTIFACT_DATE: ${{ needs.release-policy.outputs.artifact_date }} + RELEASE_CHANNEL: ${{ needs.release-policy.outputs.channel }} RELEASE_MOVE_TAG: ${{ needs.release-policy.outputs.move_tag }} RELEASE_PRERELEASE: ${{ needs.release-policy.outputs.prerelease }} RELEASE_TAG: ${{ needs.release-policy.outputs.release_tag }} @@ -168,6 +172,9 @@ jobs: if [[ $RELEASE_PRERELEASE == 'true' ]]; then args+=(--prerelease) fi + if [[ $RELEASE_CHANNEL == 'stable' ]]; then + args+=(--latest) + fi if [[ $first_publish == true && $RELEASE_MOVE_TAG == 'true' ]]; then args+=(--move-tag) fi @@ -190,32 +197,32 @@ jobs: macos_arm_pkg=$(find_one_optional "$artifact_root" "$macos_arm_pkg_name") macos_x86_pkg=$(find_one_optional "$artifact_root" "$macos_x86_pkg_name") - publish_asset "$linux_x86_tgz" "$linux_x86_tgz_name" \ + publish_asset "$linux_x86_tgz" 'pvs-linux-x86_64.tgz' \ 'pvs-*-*-linux-x86_64.tgz' \ 'pvs*-ix86_64-Linux-sbclisp.tgz' \ 'pvs-linux-x86_64.tgz' - publish_asset "$linux_arm_tgz" "$linux_arm_tgz_name" \ + publish_asset "$linux_arm_tgz" 'pvs-linux-aarch64.tgz' \ 'pvs-*-*-linux-aarch64.tgz' \ 'pvs*-aarch64-Linux-sbclisp.tgz' \ 'pvs-linux-aarch64.tgz' - publish_asset "$macos_arm_tgz" "$macos_arm_tgz_name" \ + publish_asset "$macos_arm_tgz" 'pvs-macos-arm64.tgz' \ 'pvs-*-*-macos-arm64.tgz' \ 'pvs*-arm-MacOSX-sbclisp.tgz' \ 'pvs-macos-arm64.tgz' - publish_asset "$macos_x86_tgz" "$macos_x86_tgz_name" \ + publish_asset "$macos_x86_tgz" 'pvs-macos-x86_64.tgz' \ 'pvs-*-*-macos-x86_64.tgz' \ 'pvs*-ix86-MacOSX-sbclisp.tgz' \ 'pvs-macos-x86_64.tgz' if [[ -n $macos_arm_pkg ]]; then - publish_asset "$macos_arm_pkg" "$macos_arm_pkg_name" \ + publish_asset "$macos_arm_pkg" 'pvs-macos-arm64.pkg' \ 'pvs-*-*-macos-arm64.pkg' \ 'pvs*-arm-MacOSX-sbclisp.pkg' \ 'pvs-macos-arm64.pkg' fi if [[ -n $macos_x86_pkg ]]; then - publish_asset "$macos_x86_pkg" "$macos_x86_pkg_name" \ + publish_asset "$macos_x86_pkg" 'pvs-macos-x86_64.pkg' \ 'pvs-*-*-macos-x86_64.pkg' \ 'pvs*-ix86-MacOSX-sbclisp.pkg' \ 'pvs-macos-x86_64.pkg' @@ -230,14 +237,14 @@ jobs: echo "- Release channel: \`${{ needs.release-policy.outputs.channel }}\`" echo "- Uploaded assets:" artifact_prefix="pvs-${RELEASE_ARTIFACT_BRANCH}-${RELEASE_ARTIFACT_DATE}" - echo " - \`${artifact_prefix}-linux-aarch64.tgz\`" - echo " - \`${artifact_prefix}-linux-x86_64.tgz\`" - echo " - \`${artifact_prefix}-macos-arm64.tgz\`" - echo " - \`${artifact_prefix}-macos-x86_64.tgz\`" + echo " - \`pvs-linux-aarch64.tgz\`" + echo " - \`pvs-linux-x86_64.tgz\`" + echo " - \`pvs-macos-arm64.tgz\`" + echo " - \`pvs-macos-x86_64.tgz\`" if find "$RUNNER_TEMP/release-artifacts" -type f -name "${artifact_prefix}-macos-arm64.pkg" -print -quit | grep -q .; then - echo " - \`${artifact_prefix}-macos-arm64.pkg\`" + echo " - \`pvs-macos-arm64.pkg\`" fi if find "$RUNNER_TEMP/release-artifacts" -type f -name "${artifact_prefix}-macos-x86_64.pkg" -print -quit | grep -q .; then - echo " - \`${artifact_prefix}-macos-x86_64.pkg\`" + echo " - \`pvs-macos-x86_64.pkg\`" fi } >> "$GITHUB_STEP_SUMMARY" diff --git a/.gitignore b/.gitignore index 644f9a758..853da359c 100644 --- a/.gitignore +++ b/.gitignore @@ -9,6 +9,7 @@ /doc/language/pvs-doc.el /pvs /pvsio +metadata.json /TAGS pvs-patches/patch* autom4te.cache @@ -85,4 +86,9 @@ python/src/.DS_Store python/.settings/org.eclipse.core.resources.prefs .project -.vagrant \ No newline at end of file +.vagrant + +lib/pvs2c +lib/Makefile +lib/Makefile.bak +nasalib/ \ No newline at end of file diff --git a/Makefile.in b/Makefile.in index 4c653fe9f..a6d65f957 100644 --- a/Makefile.in +++ b/Makefile.in @@ -66,6 +66,8 @@ QUICKLISP_HOME ?= $(HOME)/quicklisp QUICKLISP_SETUP ?= $(QUICKLISP_HOME)/setup.lisp PVS_BUILD_CACHE ?= $(abspath .build/cache) PVS_BUILD_LOGDIR ?= $(abspath .build/log) +PYTHON3 ?= python3 +GENERATE_BUILD_METADATA = $(PYTHON3) "$(PVSPATH).github/scripts/generate-build-metadata.py" --version "$(VERSION)" --platform "$(PLATFORM)" --toolchain "sbcl=$(SBCL_VERSION)" --toolchain "allegro=$(ALLEGRO_VERSION)" # If SBCL_HOME is set, it is preferred over SBCL; useful when testing # PVS in different SBCL versions @@ -535,6 +537,11 @@ devel : $(allegro-devel) runtime : $(sbcl-rt) # $(allegro-rt) +all devel runtime : + @$(GENERATE_BUILD_METADATA) --output metadata.json --artifact-root . \ + --artifact pvs.asd \ + --artifact "$(bindir)" --artifact "yices/$(PLATFORM)" + # Quicklisp is a package manager for lisp; see src/quicklisp.lisp for details. # The install location is configurable so CI/release builds can avoid mutating # the builder's home-directory init files. @@ -721,6 +728,7 @@ platforms = ix86_64-Linux,ix86-MacOSX,arm-MacOSX comma:= , clean : + -rm -f metadata.json -rm $(pvs-parser-out) -for d in $(subst $(comma), ,$(fasldirs)) ; do \ rm -rf $$d; \ @@ -735,6 +743,7 @@ clean : done distclean : + rm -f metadata.json for e in $(subst $(comma), ,$(faslexts)) ; do \ find . -type f -name \*.$$e -exec rm \{\} \; ; \ done @@ -784,6 +793,9 @@ define create-distdir || exit 1; \ fi; \ done + @$(GENERATE_BUILD_METADATA) --output "$(DISTDIR)/metadata.json" --artifact-root "$(DISTDIR)" \ + --artifact pvs.asd --artifact "bin/$(PLATFORM)" --artifact "yices/$(PLATFORM)" + @cp -f "$(DISTDIR)/metadata.json" metadata.json endef allegro-distdir: $(ALLEGRO_DISTFILES) @@ -803,6 +815,9 @@ sbclisp-distdir: $(SBCLISP_DISTFILES) *) : ;; \ esac @"./.github/scripts/strip-runtime-debug-info.sh" --runtime-dir "$(DISTDIR)/bin/$(PLATFORM)/runtime" + @$(GENERATE_BUILD_METADATA) --output "$(DISTDIR)/metadata.json" --artifact-root "$(DISTDIR)" \ + --artifact pvs.asd --artifact "bin/$(PLATFORM)" --artifact "yices/$(PLATFORM)" + @cp -f "$(DISTDIR)/metadata.json" metadata.json dist-gzip: dist-allegro-gzip dist-sbclisp-gzip diff --git a/emacs/pvs-ilisp.el b/emacs/pvs-ilisp.el index 2a08b63ed..9cf8f9ba9 100644 --- a/emacs/pvs-ilisp.el +++ b/emacs/pvs-ilisp.el @@ -1063,7 +1063,10 @@ is multiple lines and let the user decide what to do." message "\n" output "\n" prompt)) (if noninteractive (if pvs-validating - (progn (pvs-message "ERROR: %s" output) t) + (progn (if (string-match "IGNORE-ERR" output) + (pvs-message output) + (pvs-message "ERROR: %s" output)) + t) (error output)) (message "Preserve break") (pvs-bury-output) diff --git a/emacs/pvs-utils.el b/emacs/pvs-utils.el index 2dd55f257..3d48dd826 100644 --- a/emacs/pvs-utils.el +++ b/emacs/pvs-utils.el @@ -639,7 +639,7 @@ The save-pvs-file command saves the PVS file of the current buffer." (if buff (with-current-buffer buff (save-buffer) - (setq buffer-modified nil)) + (set-buffer-modified-p nil)) (save-buffer)) buff) (save-buffer))) diff --git a/proveit.in b/proveit.in index 54bcd3c63..1e9438042 100755 --- a/proveit.in +++ b/proveit.in @@ -14,11 +14,11 @@ # # Mariano Moscato (01/28/2025) # -# Script for batch proving in PVS -# +# Script for batch proving in PVS +# normalize_dir() { - case $1 in + case "$1" in */) printf '%s\n' "$1" ;; *) printf '%s/\n' "$1" ;; esac @@ -26,14 +26,14 @@ normalize_dir() { resolve_script_dir() { target=$1 - case $target in + case "$target" in */*) ;; *) target=`command -v "$target"` || return 1 ;; esac while [ -h "$target" ] do link=`readlink "$target"` || return 1 - case $link in + case "$link" in /*) target=$link ;; *) target=`dirname "$target"`/$link ;; esac @@ -71,7 +71,6 @@ PVS_RETURN_VALUE_MISSED_FORMS=142 # PVS' return value indicating missed (ie, not EXT=.summary # Extension for proof status summary file -PVSBIN=pvsbin # PVS directory of binary files LISPFORCE=t LISPIMPORT=nil LISPSCRIPTS=t @@ -81,11 +80,11 @@ LISPTRACES=nil LISPTXTPROOFS=nil LISPTEXPROOFS=nil LISPTYPECHECK=nil -LISPDEPENDENCIES=nil LISPAUTOFIX=nil LISPRETRYWITHTCCS=nil +LISPPURGE=nil PVSTIMEOUT= -LISPDEFAULTPROOFSCRIPT=nil +LISPDEFAULTPROOFSTEP=nil PRELUDEXT= DISABLE= ENABLE= @@ -102,18 +101,20 @@ LISPALTSUMMARIESMODE= reset_vars() { FILENOTFOUND= ARG= - OPTS= + OPTS= OUTFILE= LOGFILE= + DEPENDENCIES= + DEPFILE= PVSCONTEXT= - PVSFILE= + PVSFILENAME= THFS= - THEORIES= - LISPDEPENDENCIES=nil + THEORIES= LISPAUTOFIX=nil LISPRETRYWITHTCCS=nil + LISPPURGE=nil PVSTIMEOUT= - LISPDEFAULTPROOFSCRIPT=nil + LISPDEFAULTPROOFSTEP=nil } all_opt() { @@ -127,37 +128,32 @@ all_opt() { fi LISPIMPORT=t LISPSCRIPTS=nil - LISPDEPENDENCIES=relative + LISPPURGE=t fi } # $ARG has the general form -# | [.pvs] | [@],..,, where +# | [.pvs] | [@],..,, where # has the form [.:..:] compile_infile_name() { # If , set context to and pvsfile to top.pvs - if [ -d $ARG ]; then - PVSCONTEXT=$ARG - + if [ -d "$ARG" ]; then + PVSCONTEXT=`readlink -f $ARG` if [ -z "$OUTFILE" ]; then - # if ARG contains a slash, it is replaced by '-' since PVS does not - # accept library names containing that symbol ('-'). - OUTFILE=`echo $ARG | sed "s#/#-#g" ` - OUTFILE=$OUTFILE$EXT + OUTFILE=`basename -- "$ARG"`$EXT fi - PVSFILE=`basename $TOP .pvs` - if [ -f $PVSCONTEXT/$PVSFILE.pvs -o "$LISPAUTOTOP" = "t" ]; then + # If , set context to its dirname and pvsfile to its base name + PVSFILENAME=`basename $TOP .pvs` + if [ -f $PVSCONTEXT/$PVSFILENAME.pvs -o "$LISPAUTOTOP" = "t" ]; then all_opt else - FILENOTFOUND="$PVSCONTEXT/$PVSFILE.pvs" + FILENOTFOUND="$PVSCONTEXT/$PVSFILENAME.pvs" fi - LISPDEPENDENCIES=relative - # If , set context to its dirname and pvsfile to its base name else - case $ARG in + case "$ARG" in *@*@*) echo "Error: at most one @-sign can be provided in $ARG" exit 1;; @@ -166,16 +162,14 @@ compile_infile_name() { THFS=`echo $ARG | sed -e 's/,$//' -e "s/[^@]*@//"` if [ -z "$predir" ]; then PVSCONTEXT=$(pwd -P) - else - if [ -d "$predir" ]; then - PVSCONTEXT=$predir - else - echo "Error: $predir is not a directory" - exit 1 - fi + elif [ -d "$predir" ]; then + PVSCONTEXT=`readlink -f $predir` + else + echo "Error: $predir is not a directory" + exit 1 fi if [ "$THFS" ]; then - PVSFILE=$THFS + PVSFILENAME=$THFS THEORIES=`echo $THFS | sed -e "s/\.[^,]*,/,/g" -e "s/\.[^,]*//"` else echo "Error: At least one theory has to be specified in $ARG" @@ -183,9 +177,9 @@ compile_infile_name() { fi;; *) PVSCONTEXT=$(cd "$(dirname $ARG)" && pwd -P) - PVSFILE=`basename $ARG .pvs` - if [ ! -f $PVSCONTEXT/$PVSFILE.pvs ]; then - FILENOTFOUND="$PVSCONTEXT/$PVSFILE.pvs" + PVSFILENAME=`basename $ARG .pvs` + if [ ! -f $PVSCONTEXT/$PVSFILENAME.pvs ]; then + FILENOTFOUND="$PVSCONTEXT/$PVSFILENAME.pvs" if [ -z "$NOFILE" ]; then echo "Error: File $FILENOTFOUND not found" exit 1; @@ -196,33 +190,32 @@ compile_infile_name() { } strip_ext() { - echo "$1" | sed -e "s/\(.*\)\..*/\1/g" + echo "$1" | sed -e "s/\(.*\)\..*/\1/g" } # If necessary, set the name of the output file # compile_outfile_names() { - dir=$OUTDIR if [ -z "$OUTFILE" ]; then - if [ -z "$dir" ]; then - dir=$PVSCONTEXT + if [ -z "$OUTDIR" ]; then + OUTDIR=$PVSCONTEXT fi - OUTFILE=$PVSFILE$EXT - else - if [ -z "$dir" ]; then + OUTFILE=$PVSFILENAME$EXT + elif [ -z "$OUTDIR" ]; then dir=`dirname $OUTFILE` - fi + OUTDIR=`readlink -f $dir` fi base=`basename $OUTFILE` - BASEOUT=`strip_ext $base` - if [ "$BASEOUT" = $base ]; then - base=$BASEOUT$EXT + OUTBASENAME=`strip_ext $base` + if [ "$OUTBASENAME" = $base ]; then + base=$OUTBASENAME$EXT fi - if [ "$dir" ]; then - OUTFILE=$dir/$base - LOGFILE=$dir/$BASEOUT.log + if [ "$OUTDIR" ]; then + OUTFILE=$OUTDIR/$base + LOGFILE=$OUTDIR/$OUTBASENAME.log + DEPFILE=$OUTDIR/$OUTBASENAME.dep fi - if [ "$LISPTYPECHECK" = "t" ]; then + if [ "$LISPTYPECHECK" = "t" ]; then OUTFILE=$OUTFILE-tc fi @@ -231,7 +224,7 @@ compile_outfile_names() { # Translate a list l1,...,ln into (l1 .. ln) list_to_lisp() { if [ -z "$1" ] - then + then echo nil else echo "(\"$1\")" | sed -e "s/,/\" \"/g" @@ -254,22 +247,15 @@ cleanup() { then if [ "$PVSCONTEXT" ]; then if [ "$BINARIESONLY" ]; then - PVSCONTEXT_CTXT="$PVSCONTEXT/.pvscontext $PVSCONTEXT/$PVSBIN/*.bin" + PVSCONTEXT_CTXT="$PVSCONTEXT/.pvscontext $PVSCONTEXT/pvsbin/*.bin" else - PVSCONTEXT_CTXT="$PVSCONTEXT/.pvscontext $PVSCONTEXT/$PVSBIN/*.*" + PVSCONTEXT_CTXT="$PVSCONTEXT/.pvscontext $PVSCONTEXT/orphaned-proofs.prf $PVSCONTEXT/pvsbin/*.*" fi - fi - if [ "$LOGFILE" ]; then - LOGFILE_RELATIVE_PATH="$LOGFILE" fi - if [ "$OUTFILE" ]; then - OUTFILE_RELATIVE_PATH="$OUTFILE" - fi - if [ -z "$QUIET" ] - then - echo "Removing $PVSCONTEXT_CTXT $OUTFILE_RELATIVE_PATH $LOGFILE_RELATIVE_PATH" + if [ -z "$QUIET" ]; then + echo "Removing $PVSCONTEXT_CTXT $OUTFILE $LOGFILE $DEPFILE" fi - rm -f $PVSCONTEXT_CTXT $OUTFILE_RELATIVE_PATH $LOGFILE_RELATIVE_PATH + rm -f $PVSCONTEXT_CTXT $OUTFILE $LOGFILE $DEPFILE fi } @@ -277,7 +263,7 @@ cleanup() { # usage() { readVersion - + echo "NAME proveit $VERSION -- runs PVS in batch mode @@ -288,7 +274,7 @@ SYNOPSIS DESCRIPTION Prove all theories in the input files, e.g., - + \$ proveit Prove all theories imported in /top.pvs @@ -299,54 +285,53 @@ DESCRIPTION Prove all theries in .pvs and their dependencies ADVANCED USE - In the more general form, a context, a list of theories, and a list of - formulas are specified using the syntax <[ctxt]@thf1,..,thfn>, where - is a directory and each has the form with being a + In the more general form, a context, a list of theories, and a list of + formulas are specified using the syntax <[ctxt]@thf1,..,thfn>, where + is a directory and each has the form with being a theory and a list of formulas in . Only formulas specified this way are proven by PVS. In this case, the proof status is saved - in .summary in . For example, to prove formulas and - in theory in the current context, type: + in .summary in . For example, to prove formulas and + in theory in the current context, type: \$proveit @.: - Note that, when the target is a directory (as in the first example in the + Note that, when the target is a directory (as in the first example in the Description section), all the files in its pvsbin subfolder are overwritten. OPTIONS - Options are processed in the order they appear. One letter options can be + Options are processed in the order they appear. One letter options can be combined. - -a|--all equivalent to -ciq - --auto-fix [] try sibling proofs on unfinished branchs ( is the maximum - acceptable distance between the current branch and the sibling + -a|--all equivalent to -ciq + --auto-fix [] try sibling proofs on unfinished branchs ( is the maximum + acceptable distance between the current branch and the sibling which proof is to be tried; default value is 2) --backup-summaries backup summary files instead of replacing them (disable by default) - -c|--clean remove .pvscontext and binary files in the pvsbin folder before proving - -C|--clean-only just remove .pvscontext and binary files in the pvsbin folder - (do not typecheck nor prove) - --clean-all just remove .pvscontext and all files in the pvsbin folder - (do not typecheck nor prove) + -c|--clean remove .pvscontext and binary files in the pvsbin folder before proving or type-checking + -C|--clean-only remove .pvscontext and binary files in the pvsbin folder, and quit + --clean-all remove .pvscontext, orphaned-proofs.prf, and all files in pvsbin, and quit -d|--dir use as default directory of summary files - --dependencies [relative|fullpath] compute theory dependencies and save them in - pvsbin/.dep. - --default-script default prooflite script to be tried on unfinished branches + --dependencies [] compute theory dependencies, where can be relative (default) or fullpath, + and save them in /.dep (same directory as summary files) + --default-proof default proof step to be tried on unfinished branches --disable disable external oracles o1,...,on --disable-oracles disable any external oracle --enable enable external oracles o1,..,on. Overwrite --disable - . use as default extension of summary files -f|--force force proof reruns (default) - ~f|--no-force don't force proof reruns + --no-force don't force proof reruns -h|--help print this message -i|--importchain prove chain of imported theories (set --no-scripts) - ~i|--no-importchain don't prove chain of imported theories (default) + --no-importchain don't prove chain of imported theories (default) --lisp specify lisp version; is one of allegro,cmulisp -l|--log log all information generated by PVS in .log - ~l|--no-log don't log PVS information (default) + --no-log don't log PVS information (default) -o|--out save the proof status summary in . - -p|--prelude-ext load prelude extensions p1,..,pn - ~p|--no-prelude-ext don't load any prelude extension - -q|--quiet print only untried and unfinished proofs per theory, and grand total + -p|--prelude-ext load prelude extensions p1,..,pn + --no-prelude-ext don't load any prelude extension + --purge purge non-default proofs from proved formulas (default on directories) + --no-purge don't purge non-default proofs + -q|--quiet print only untried and unfinished proofs per theory, and grand total -s|--scripts install ProofLite scripts (default) - ~s|--no-scripts don't install ProofLite scripts + --no-scripts don't install ProofLite scripts --tex generate LaTeX proof files in directory pvstex --no-tex don't generate LaTeX proof files (default) --txt generate text proof files in directory pvstxt @@ -361,8 +346,8 @@ OPTIONS --version print version information and exit -w|--write-scripts write proofs as prooflite scripts into separate files (disabled by default, this option is omitted in typecheck-only mode.) - --summary-mode alternative summary mode, where can be md for Markdown, or csv - for comma-separated values. + --summary-mode summary mode, where can be md for Markdown, or csv + for comma-separated values SEE ALSO provethem -- for iterating proveit on a list of directories @@ -385,14 +370,14 @@ error_output() { } }' \ -e '/^Typechecking/h' \ - -e '/Proof summary/,/Grand Totals/p' $OUTFILE + -e '/Proof summary/,/Grand Totals/p' $OUTFILE if [ -z "$QUIET" ]; then cat $OUTFILE | \ sed -e "s+^+Error: \1 ($ARG) +" \ -e 's/"//g' -e 's/<\/pvserror>//g' \ -e 's/^Error/*** Error/gp'\ -e 's/^\*\*\* Warning/*** Warning/gp'\ - -e '/^\*\*\*.*/d' + -e '/^\*\*\*.*/d' else cat $OUTFILE | \ sed -n -e "s+^\"\(.*\)\"<\/pvserror>+Error: \1 ($ARG) \2 +p" \ @@ -450,7 +435,7 @@ quiet_output() { /unchecked/H /untried/H }'\ - -e '/Theory totals/ { + -e '/Theory totals/ { i\ x;p;g;p @@ -473,84 +458,87 @@ quiet_output() { H;g /\.\.\.\./p }'\ - -e '/^Grand Totals:/p' + -e '/^Grand Totals:/p' fi } process_opts() { while [ $# -gt 0 ] do - case $1 in - -a|all|--all) + case "$1" in + -a|--all) all_opt;; - -c|-clean|--clean) + -c|--clean) CLEAN=yes;; - ~c|-no-clean|--no-clean) + --no-clean) CLEAN=;; - -f|-force|--force) + -f|--force) LISPFORCE=t;; - ~f|-no-force|--no-force) + --no-force) LISPFORCE=nil;; - -i|-importchain|--importchain) + -i|--importchain) LISPSCRIPTS=nil LISPIMPORT=t;; - ~i|-no-importchain|--no-importchain) + --no-importchain) LISPIMPORT=nil;; - -w|-write-scripts|--write-scripts) + -w|--write-scripts) LISPWRITESCRIPTS=t;; - -s|-scripts|--scripts) + -s|--scripts) LISPSCRIPTS=t;; - ~s|-no-scripts|--no-scripts) + --no-scripts) LISPSCRIPTS=nil;; - -T|-Typecheck|--Typecheck|-typecheck-only|--typecheck-only) + -T|--typecheck-only) LISPTYPECHECK=t;; - -traces|--traces) + --traces) LOG=yes LISPTRACES=t;; - -no-traces|--no-traces) + --no-traces) LISPTRACES=nil;; - -txt|--txt) + --txt) LISPTXTPROOFS=t;; - -no-txt|--no-txt) + --no-txt) LISPTXTPROOFS=nil;; - -tex|--tex) + --tex) LISPTEXPROOFS=t;; - -no-tex|--no-tex) + ---no-tex) LISPTEXPROOFS=nil;; - -l|-log|--log) + -l|--log) LOG=yes;; - ~l|-no-log|--no-log) + --no-log) LOG=;; - ~p|-no-prelude-ext|--no-prelude-ext) + --no-prelude-ext) PRELUDEXT=;; - -q|-quiet|--quiet) + -q|--quiet) QUIET=yes;; - -v|-verbose|--verbose) + -v|--verbose) QUIET=;; - --*) + --*) echo "Error: $1 is not a valid option" exit 1;; + -) + echo "Error: - is not a valid option" + exit 1;; -*) opts=`echo "$1" | sed -e s/-//g -e "s/\(.\)/\1 /g"` for opt in $opts; do - case $opt in - a) + case "$opt" in + a) all_opt;; - c) + c) CLEAN=yes;; C) QUIET= BINARIESONLY=t CLEAN=only;; - f) + f) LISPFORCE=t;; s) LISPSCRIPTS=t;; w) LISPWRITESCRIPTS=t;; - v) + v) QUIET=;; - i) + i) LISPSCRIPTS=nil LISPIMPORT=t;; l) @@ -559,35 +547,10 @@ process_opts() { QUIET=yes;; T) LISPTYPECHECK=t;; - *) - usage + *) echo "Error: -$opt is not a valid option" exit 1;; esac - done;; - ~*) - opts=`echo "$1" | sed -e s/~//g -e "s/\(.\)/\1 /g"` - for opt in $opts; do - case $opt in - c) - CLEAN=;; - f) - LISPFORCE=nil;; - i) - LISPIMPORT=nil;; - s) - LISPSCRIPTS=nil;; - w) - LISPWRITESCRIPTS=nil;; - l) - LOG=;; - p) - PRELUDEXT=;; - *) - usage - echo "Error: ~$opt is not a valid option" - exit 1;; - esac done esac shift @@ -624,18 +587,21 @@ proveit() { fi cleanup - + if [ "$FILENOTFOUND" -a "$LISPAUTOTOP" != "t" ]; then if [ -z "$CLEAN" ]; then echo "Error: File $FILENOTFOUND not found" fi exit 1 fi - + echo "Processing $ARG. Writing output to file $OUTFILE" if [ "$LOG" ]; then echo "Logging PVS information in $LOGFILE" fi + if [ "$DEPENDENCIES" ]; then + echo "Saving theory dependencies ($DEPENDENCIES) in $DEPFILE" + fi if [ -z "$QUIET" ]; then if [ "$PRELUDEXT" ]; then echo "Loading prelude extensions: $PRELUDEXT" @@ -652,19 +618,16 @@ proveit() { fi if [ "$LISPIMPORT" = "t" ]; then echo "Proving chain of imported theories" - fi - if [ "$LISPDEPENDENCIES" != "nil" ]; then - echo "Saving theory dependencies ($LISPDEPENDENCIES) in directory pvsbin" fi if [ ! -z "$LISPALTSUMMARIESMODE" ]; then echo "Summaries will be also reported in alternative format: $(echo $LISPALTSUMMARIESMODE | sed 's/,/ and /')." fi if [ "$LISPSCRIPTS" != "t" ]; then echo "ProofLite scripts won't be installed" - fi + fi if [ "$LISPWRITESCRIPTS" = "t" ]; then echo "Proofs wish/ill be stored as ProofLite scripts in .prl files." - fi + fi if [ "$LISPAUTOTOP" = "t" ]; then echo "Top file will be automatically generated." fi @@ -686,8 +649,11 @@ proveit() { if [ "$LISPRETRYWITHTCCS" != "nil" ]; then echo "Retry-with-tccs enabled" fi - if [ "$LISPDEFAULTPROOFSCRIPT" != "nil" ]; then - echo "Default proof script $LISPDEFAULTPROOFSCRIPT" + if [ "$LISPPURGE" = "t" ]; then + echo "Purge non-default proofs enabled" + fi + if [ "$LISPDEFAULTPROOFSTEP" != "nil" ]; then + echo "Default proof script $LISPDEFAULTPROOFSTEP" fi if [ "$PVSTIMEOUT" ]; then echo "Timeout set at $PVSTIMEOUT secs." @@ -696,11 +662,15 @@ proveit() { export PROVEITARG="$ARG" export PROVEITPVSCONTEXT="$PVSCONTEXT" - if [ -f $PVSCONTEXT/$PVSFILE.pvs -o "$LISPAUTOTOP" = "t" ]; then - export PROVEITPVSFILE="$PVSFILE" + if [ -f $PVSCONTEXT/$PVSFILENAME.pvs -o "$LISPAUTOTOP" = "t" ]; then + export PROVEITPVSFILENAME="$PVSFILENAME" else - export PROVEITPVSFILE="" - fi + export PROVEITPVSFILENAME="" + fi + export PROVEITOUTDIR="$OUTDIR" + export PROVEITOUTBASENAME="$OUTBASENAME" + export PROVEITDEPENDENCIES="$DEPENDENCIES" + export PROVEITDEPFILE="$DEPFILE" export PROVEITLISPIMPORT="$LISPIMPORT" export PROVEITLISPSCRIPTS="$LISPSCRIPTS" export PROVEITLISPWRITESCRIPTS="$LISPWRITESCRIPTS" @@ -710,7 +680,6 @@ proveit() { export PROVEITLISPTYPECHECK="$LISPTYPECHECK" export PROVEITLISPTXTPROOFS="$LISPTXTPROOFS" export PROVEITLISPTEXPROOFS="$LISPTEXPROOFS" - export PROVEITLISPDEPENDENCIES="$LISPDEPENDENCIES" export PROVEITLISPALTSUMMARIESMODE="`list_to_lisp $LISPALTSUMMARIESMODE`" export PROVEITLISPPRELUDEXT="`list_to_lisp $PRELUDEXT`" export PROVEITLISPDISABLE="`list_to_lisp $DISABLE`" @@ -719,31 +688,32 @@ proveit() { export PROVEITLISPTHEORIES="`list_to_lisp $THEORIES`" export PROVEITLISPAUTOFIX="$LISPAUTOFIX" export PROVEITLISPRETRYWITHTCCS="$LISPRETRYWITHTCCS" - export PROVEITLISPDEFAULTPROOFSCRIPT="$LISPDEFAULTPROOFSCRIPT" + export PROVEITLISPPURGE="$LISPPURGE" + export PROVEITLISPDEFAULTPROOFSTEP="$LISPDEFAULTPROOFSTEP" - export PROVEITLISPOUTDIR=$dir - export PROVEITLISPOUTBASENAME=$BASEOUT - if [ "$DEBUG" ]; then readVersion export DEBUG echo "QUIET=$QUIET" - echo "PROVEITVERSION=$VERSION" echo "OUTFILE=$OUTFILE" echo "LOGFILE=$LOGFILE" + echo "PROVEITVERSION=$VERSION" echo "export PROVEITARG=$PROVEITARG" echo "export PROVEITPVSCONTEXT=$PROVEITPVSCONTEXT" - echo "export PROVEITPVSFILE=$PROVEITPVSFILE" + echo "export PROVEITPVSFILENAME=$PROVEITPVSFILENAME" + echo "export PROVEITOUTDIR=$PROVEITOUTDIR" + echo "export PROVEITOUTBASENAME=$PROVEITOUTBASENAME" + echo "export PROVEITDEPENDENCIES=$PROVEITDEPENDENCIES" + echo "export PROVEITDEPFILE=$PROVEITDEPFILE" echo "export PROVEITLISPIMPORT=$PROVEITLISPIMPORT" echo "export PROVEITLISPSCRIPTS=$PROVEITLISPSCRIPTS" echo "export PROVEITLISPWRITESCRIPTS=$PROVEITLISPWRITESCRIPTS" echo "export PROVEITLISPTRACES=$PROVEITLISPTRACES" - echo "export PROVEITLISPFORCE=$PROVEITLISPFORCE" + echo "export PROVEITLISPFORCE=$PROVEITLISPFORCE" echo "export PROVEITLISPAUTOTOP=$LISPAUTOTOP" echo "export PROVEITLISPTYPECHECK=$PROVEITLISPTYPECHECK" echo "export PROVEITLISPTXTPROOFS=$PROVEITLISPTXTPROOFS" echo "export PROVEITLISPTEXPROOFS=$PROVEITLISPTEXPROOFS" - echo "export PROVEITLISPDEPENDENCIES=$PROVEITLISPDEPENDENCIES" echo "export PROVEITLISPALTSUMMARIESMODE=$PROVEITLISPALTSUMMARIESMODE" echo "export PROVEITLISPPRELUDEXT=$PROVEITLISPPRELUDEXT" echo "export PROVEITLISPDISABLE=$PROVEITLISPDISABLE" @@ -752,9 +722,10 @@ proveit() { echo "export PROVEITLISPTHEORIES=$PROVEITLISPTHEORIES" echo "export PROVEITLISPAUTOFIX=$PROVEITLISPAUTOFIX" echo "export PROVEITLISPRETRYWITHTCCS=$PROVEITLISPRETRYWITHTCCS" - echo "export PROVEITLISPDEFAULTPROOFSCRIPT=$PROVEITLISPDEFAULTPROOFSCRIPT" + echo "export PROVEITLISPPURGE=$PROVEITLISPPURGE" + echo "export PROVEITLISPDEFAULTPROOFSTEP=$PROVEITLISPDEFAULTPROOFSTEP" fi - + if [ $PVSTIMEOUT ]; then TIMEOUTARG="-timeout $PVSTIMEOUT" else @@ -764,17 +735,17 @@ proveit() { if [ "$DEBUG" ]; then echo "About to run: ""$PVSPATH""pvs -raw $PVSLISP $TIMEOUTARG -E \"(proveit)\" > $OUTFILE 2>&1" fi - + "$PVSPATH"pvs -raw $PVSLISP $TIMEOUTARG -E "(proveit)" > $OUTFILE 2>&1 ret_value=$? - + if [ "$DEBUG" ]; then echo "PVS return value: $ret_value" fi if [ $ret_value -ne 0 ] && [ $ret_value -ne $PVS_RETURN_VALUE_MISSED_FORMS ]; then error_output - exit $ret_value + exit $ret_value fi pvs_output fi @@ -788,148 +759,180 @@ proveit() { ret_value=0 reset_vars -while [ $# -gt 0 ] -do - case $1 in - --debug) - DEBUG=yes;; - -h|-help|--help) - usage - exit 0;; - -version|--version) - readVersion - echo $VERSION - exit 0;; - .*) - EXT=$1;; - -lisp|--lisp) - case $2 in - allegro) - LISP='allegro';; - cmulisp) - LISP='cmulisp' - PVSBIN='PVSBIN';; - sbclisp) - LISP='sbclisp' - PVSBIN='PVSBIN';; - *) - echo "Error: Only allegro, cmulisp, and sbcl are currently available" - exit 1;; - esac - if [ "$LISP" ]; then - PVSLISP="-lisp $LISP" - fi - shift;; - -d|-dir|--dir) - OUTDIR=$2 - if [ ! -e "$OUTDIR" ]; then - mkdir $OUTDIR - fi - if [ ! -d "$OUTDIR" ]; then - echo "Error: $OUTDIR is not a directory" - exit 1 - fi - shift;; - -t|-top|--top) - TOP=$2 - shift;; - -generate-top|--generate-top) - LISPAUTOTOP=t;; - -Clean|--Clean) - echo "The option $1 is not longer supported. Please use --clean-all instead." - exit 1;; - -C|-clean-only|--clean-only) - QUIET= - BINARIESONLY=t - CLEAN=only;; - -clean-all|--clean-all) - QUIET= - BINARIESONLY= - CLEAN=only;; - -o|-out|--out) - if [ -d "$2" ]; then - echo "Error: $2 is a directory" - exit 1 - else - OUTFILE=$2 - fi - shift;; - --backup-summaries) - BACKUP_SUMMARIES=t;; - -p|-prelude-ext|--prelude-ext) - PRELUDEXT=`append $2 $PRELUDEXT` - shift;; - -disable|--disable) - DISABLE=`append $2 $DISABLE` - shift;; - -disable-oracles|--disable-oracles) - DISABLE="_";; - -enable|--enable) - ENABLE=`append $2 $ENABLE` - shift;; - --retry-with-tccs) - LISPRETRYWITHTCCS=t;; - --auto-fix) - LISPAUTOFIX=2 - if echo $2 | grep -qE '^[+-]?[0-9]+$'; then - LISPAUTOFIX=$2 +while [ $# -gt 0 ]; do + case "$1" in + --debug) + DEBUG=yes;; + -h|--help) + usage + exit 0;; + -v|--version) + readVersion + echo $VERSION + exit 0;; + .*) + echo "Error: DEPRECATED USAGE. Extension of summary files is $EXT" + exit 1;; + --lisp) shift - fi;; - -dep|--dep|-dependencies|--dependencies) - if echo $2 | grep -qE '^-.*$'; then - # 'relative' by default - LISPDEPENDENCIES=relative - elif echo $2 | grep -qE '^relative$'; then - LISPDEPENDENCIES=relative + case "$1" in + allegro) + LISP=allegro;; + cmulisp) + LISP=cmulisp;; + sbclisp) + LISP=sbclisp;; + -* | "") + echo "Error: Expected --lisp " + exit 1;; + *) + echo "Error: Only allegro, cmulisp, and sbcl are currently available" + exit 1;; + esac + PVSLISP="-lisp $LISP";; + -d|--dir) shift - elif echo $2 | grep -qE '^fullpath$'; then - LISPDEPENDENCIES=fullpath + case "$1" in + -* | "") + echo "Error: Expected --dir " + exit 1;; + *) + if [ -d "$1" ]; then + OUTDIR=`readlink -f $1` + elif [ -e "$1" ]; then + echo "Error: $1 is not a directory" + exit 1 + else + mkdir $1 + OUTDIR=`readlink -f $1` + fi + esac;; + -t|--top) shift - else - echo "Error: --dependencies option must be followed by the options 'relative' or 'fullpath'. (See proveit --help for details.)" - exit 1 - fi;; - -summary-mode|--summary-mode) - if echo $2 | grep -qE '^[^-]'; then - LISPALTSUMMARIESMODE=`append $2 $LISPALTSUMMARIESMODE` + case "$1" in + -* | "") + echo "Error: Expected --dir " + exit 1;; + *) + TOP=$1 + esac;; + --generate-top) + LISPAUTOTOP=t;; + -C|--clean-only) + QUIET= + BINARIESONLY=t + CLEAN=only;; + --clean-all) + QUIET= + BINARIESONLY= + CLEAN=only;; + -o|--out) shift - else - echo "Error: --summary-mode option must be followed by the option 'md' or 'csv'. (See proveit --help for details.)" - exit 1 - fi;; - --timeout) - if echo $2 | grep -qE '^[0-9]+$'; then - PVSTIMEOUT=$2 + case "$1" in + -* | "") + echo "Error: Expected --out " + exit 1;; + *) + if [ -d "$1" ]; then + echo "Error: $1 is a directory" + exit 1 + else + OUTFILE=$1 + fi + esac;; + --backup-summaries) + BACKUP_SUMMARIES=t;; + -p|--prelude-ext) shift - else - echo "Error: --timeout option must be followed by the limit in seconds. (See proveit --help for details.)" - exit 1 - fi;; - --default-script) - if echo $2 | grep -qE '\(.*\)'; then - LISPDEFAULTPROOFSCRIPT=$2 + case "$1" in + -* | "") + echo "Error: Expected --prelude-ext " + exit 1;; + *) + PRELUDEXT=`append $1 $PRELUDEXT` + esac;; + --disable) shift - else - echo "Error: $2 does not seem to be a proof script." - exit 1 - fi;; - -*|~*) OPTS="$OPTS $1";; - *) ARG=$1 - NOFILE= - proveit - ret_value=$? - esac - shift -done + case "$1" in + -* | "") + echo "Error: Expected --disable " + exit 1;; + *) + DISABLE=`append $1 $DISABLE` + esac;; + --disable-oracles) + DISABLE="_";; + --enable) + shift + case "$1" in + -* | "") + echo "Error: Expected --disable " + exit 1;; + *) + ENABLE=`append $1 $ENABLE` + esac;; + --retry-with-tccs) + LISPRETRYWITHTCCS=t;; + --purge) + LISPPURGE=t;; + --no-purge) + LISPPURGE=nil;; + --auto-fix) + LISPAUTOFIX=2 + if echo $2 | grep -qE '^[+-]?[0-9]+$'; then + LISPAUTOFIX=$2 + shift + fi;; + --dependencies) + if [ "$2" = "relative" -o "$2" = "fullpath" ]; then + DEPENDENCIES=$2 + shift + else + DEPENDENCIES=relative + fi;; + --summary-mode) + shift + if [ "$1" = "md" -o "$1" = "csv" ]; then + LISPALTSUMMARIESMODE=`append $1 $LISPALTSUMMARIESMODE` + else + echo "Error: Expected --summary-mode [md|csv]" + exit 1 + fi;; + --timeout) + if echo $2 | grep -qE '^[0-9]+$'; then + PVSTIMEOUT=$2 + shift + else + echo "Error: Expected --timeout " + exit 1 + fi;; + --default-script) + echo "Error: DEPRECATED. Use --default-proof instead" + exit 1;; + --default-proof) + if echo $2 | grep -qE '\(.*\)'; then + LISPDEFAULTPROOFSTEP=$2 + shift + else + echo "Error: Expected --default-proof " + exit 1 + fi;; + -*) + OPTS="$OPTS $1";; + *) + ARG=$1 + NOFILE= + proveit + ret_value=$? + esac + shift +done if [ "$NOFILE" ]; then - ARG=$TOP.pvs - if [ -f $ARG -o "$CLEAN" = "only" ]; then - proveit - ret_value=$? - else - echo "[proveit] no file '$NOFILE'" - usage - fi + ARG=$TOP.pvs + if [ -f $ARG -o "$CLEAN" = "only" ]; then + proveit + ret_value=$? + fi fi exit $ret_value; diff --git a/provethem.in b/provethem.in index caed96329..b3b54b2b7 100755 --- a/provethem.in +++ b/provethem.in @@ -14,7 +14,7 @@ # # Mariano Moscato (12/07/2023) # -# Script for batch proving several libraries in PVS +# Script for batch proving several libraries in PVS # use Getopt::Long qw(GetOptionsFromString); @@ -71,7 +71,7 @@ sub readVersion(){ sub usage() { readVersion(); - + print < prove all libraries from , inclusive --to= prove all libraries to , inclusive - --top use .pvs instead of top.pvs as top theory + --top use .pvs instead of top.pvs as top theory --force force provethem to go even if there is a proveit error --lisp lisp image to be used; can be allegro, cmulisp, or sbcl - + --out save output to - + --no-color do not use colors --dry-run process but do not call proveit --verbose print summary information for all theories --version print version information and exit - - --addpath add current directory to PVS_LIBRARY_PATH (default when --clearpath) - --clearpath clear PVS_LIBRARY_PATH - - --clean-only remove .pvscontext and binary files in the pvsbin folder but - do not prove the libraries - --clean-all remove .pvscontext and all files in the pvsbin folder but do - not prove the libraries + + --clearpath clear PVS_LIBRARY_PATH + --addpath [] add to PVS_LIBRARY_PATH. If is empty, add current directory + + --clean-only remove .pvscontext and binary files in the pvsbin folder, and quit + --clean-all remove .pvscontext, orphaned-proofs.prf, and all files in pvsbin, and quit --typecheck-only typecheck but do not prove the libraries - --execute execute Unix on all libraries; Command + --execute execute Unix on all libraries; Command may refer to \%DIR\% and \%FILE\% --disable disable external oracles o1,...,on @@ -117,8 +115,9 @@ $usageln --dir use as default directory for summary files --ext use as default extension for summary files - --log log all information generated by PVS in .log + --log log all information generated by PVS in .log + --purge purge non-default proofs from proved formulas File is an ordered list of libraries to be processed by proveit. If is not provided, the file name all-libraries is assumed. Each @@ -138,7 +137,7 @@ EOF $ret_val_labels{'127'}="CMD-NOT-FOUND"; $ret_val_labels{'0'}="OK"; -GetOptions('addpath'=>\$addpath2, +GetOptions('addpath:s'=>\$addpath2, 'clean-only'=>\$clean2, 'clean-all'=>\$cleanall2, 'clearpath'=>\$clearpath2, @@ -149,6 +148,7 @@ GetOptions('addpath'=>\$addpath2, 'lisp=s'=>\$lisp2, 'log' => \$log2, 'enable=s'=>\@enable2, + 'purge'=>\$purge2, 'typecheck-only'=>\$typecheckonly2, 'after=s'=>\$after2, 'before=s'=>\$before2, @@ -168,7 +168,7 @@ GetOptions('addpath'=>\$addpath2, 'debug'=>\$debug, 'action-name=s'=>\$act, 'ret-val-label=s'=>\%ret_val_labels, - 'no-printout'=>\$no_printout, + 'no-printout'=>\$no_printout, 'pid'=>\$pid ) or exit 1; @@ -204,11 +204,11 @@ if (!$file) { $file = 'all-theories'; } else { $file = 'all-libraries'; - + print "*** Warning: input file not found. Files $file and top.pvs will be generated.\n"; $overopts .= " --generate-top"; - + opendir(current_directory, "."); my @files = readdir(current_directory); closedir(current_directory); @@ -227,8 +227,9 @@ if (!$file) { if ( scalar @files_in_subdir > 0) { push(@all_libraries,$file_in_dir); - # look into the pvsbin/top.dep file to check dependencies - $depfile = "$file_in_dir/pvsbin/$top.dep"; + # look into the dep file to check dependencies + $depfile = $dir ? "$dir/$file_in_dir.dep" : "$file_in_dir/$file_in_dir.dep"; + print "DEPFILE (1): $depfile~%"; if (-f $depfile) { open (DEPFILE,"$depfile"); while () { @@ -247,7 +248,7 @@ if (!$file) { close (DEPFILE); } else { print "*** Warning: File $depfile not found.\n"; - } + } } } } @@ -262,7 +263,7 @@ if (!$file) { $result=1; } elsif (exists $lib_deps{$b} && grep { $a eq $_ } @{$lib_deps{$b}}){ $result=-1; - } + } return $result; }; @all_libraries = sort {$lib_cmp->($a,$b)} @all_libraries; @@ -280,7 +281,7 @@ if (!$file) { $column_width=`sed -E "s/^([^ ]*) .*\$/\\1/g" $file | awk "length > max_length { max_length = length; longest_line = \$0 } END { print max_length }"`+3; -die "$usageln\n" if shift; +die "$usageln\n" if shift; my $can_accept_in_file_global_options=1; @@ -296,7 +297,7 @@ while () { "(line ",${\*all_theories_file}->input_line_number, " in $file)" unless ($can_accept_in_file_global_options); GetOptionsFromString($line, - 'addpath'=>\$addpath, + 'addpath:s'=>\$addpath, 'clean-only'=>\$clean, 'clean-all'=>\$cleanall, 'clearpath'=>\$clearpath, @@ -307,6 +308,7 @@ while () { 'lisp=s'=>\$lisp, 'log' => \$log, 'enable=s'=>\@enable, + 'purge'=>\$purge, 'typecheck-only'=>\$typecheckonly, 'after=s'=>\$after, 'before=s'=>\$before, @@ -369,6 +371,7 @@ $ext=override_scalar_option("--ext",$ext,$ext2); $lisp=override_scalar_option("--lisp",$lisp,$lisp2); $log=override_scalar_option("--log",$log,$log2); $typecheckonly=override_scalar_option("--typecheck-only",$typecheckonly,$typecheckonly2); +$purge=override_scalar_option("--purge",$purge,$purge2); $disableoracles=override_scalar_option("--disable-oracles",$disableoracles,$disableoracles2); @@ -485,14 +488,14 @@ sub iteratelibs(){ $go = "ok" if ($from eq $lib); last if $before eq $lib; - if (($go || grep { "$_" eq $lib } @dolist) && + if (($go || grep { "$_" eq $lib } @dolist) && !(grep { "$_" eq $lib } @butlist)) { $libs += 1; if (-d $lib) { $pathlib = $lib; $baselib = ""; - } elsif (-f $lib) { - ($baselib,$pathlib,$typelib) = fileparse($lib,qr{\..*}); + } elsif (-f $lib) { + ($baselib,$pathlib,$typelib) = fileparse($lib,qr{\..*}); $baselib .= $typelib; } else { die "$lib is neither a file nor a directory\n"; @@ -503,7 +506,7 @@ sub iteratelibs(){ $exe =~ s/\%OPTS\%/$opts/g; $command=""; $command .= "$exe"; - + if ($command) { if ($dryrun) { print "DRY-RUN: $command\n"; @@ -532,12 +535,12 @@ sub iteratelibs(){ } print OUTFILE "$proveout\n" if $out; - + my @warnings = ($proveout =~ m/(Warning[:]? .*)/g); if (@warnings) { $warn_msg = join("\n*** ",@warnings); } - + my @errors = ($proveout =~ m/(Error[:]? .*)/g); if (@errors) { $fail_msg = join("\n*** ",@errors); @@ -552,7 +555,7 @@ sub iteratelibs(){ if ($no_color) { print $status; } else { - print DARK RED $status; + print DARK RED $status; } $fail_msg .= " (return value: $fail)" if $verbose; if ($fail_msg) { @@ -565,7 +568,7 @@ sub iteratelibs(){ # Update my return value $return_value=$fail if ($fail > $return_value); } - + if ($fail == 0) { $status = $ret_val_labels{0}; $status = "OK" if ! $status; @@ -574,7 +577,7 @@ sub iteratelibs(){ if ($no_color) { print $status; } else { - print DARK GREEN $status; + print DARK GREEN $status; } $endln = "]\n"; print $endln; @@ -585,7 +588,8 @@ sub iteratelibs(){ # since warnings are already there. print "*** $warn_msg\n" if $warn_msg && $no_printout; - $depfile = "$lib/pvsbin/$top.dep"; + $depfile = $dir ? "$dir/$lib.dep" : "$lib/$lib.dep"; + print "DEPFILE (2): $depfile~%"; if (-f $depfile) { open (DEPFILE,"$depfile"); while () { @@ -599,7 +603,7 @@ sub iteratelibs(){ !(grep {$_ eq $deplib} @libraries) && -d $deplib && -f "$deplib/$top.pvs") { print "*** Warning: Library $deplib is out of order. It should appear before $lib in $file\n"; - } + } } else { print "*** Warning: Cannot check library order. Obsolete dep file for library $lib? Try regenerating it.\n"; } @@ -622,7 +626,7 @@ sub iteratelibs(){ } } my $mssg = "\n"; - $mssg .= "*** Number of libraries: $libs\n"; + $mssg .= "*** Number of libraries: $libs\n"; print $mssg; $summary .= $mssg; @@ -635,9 +639,9 @@ sub iteratelibs(){ return($return_value); } -# ad-hoc version of iteratelibs to apply proveit on each library in the scope +# ad-hoc version of iteratelibs to apply proveit on each library in the scope sub iterate_proveit_on_libs(){ - $execute="$PROVEIT %OVEROPTS% %OPTS% %DIR%"; + $execute="$PROVEIT --dependencies %OVEROPTS% %OPTS% %DIR%"; if(!$out){ $out="provethem.out"; @@ -649,9 +653,9 @@ sub iterate_proveit_on_libs(){ $ret_val_labels{'15'}="FAIL - terminated"; $no_printout="t"; - + # - + print "Executing shell command \"$execute\" on each library.\n" if $verbose; print "With overopts: $overopts.\n" if $verbose && $execute=~/\%OVEROPTS\%/; print "\n"; @@ -661,7 +665,7 @@ sub iterate_proveit_on_libs(){ my $totalproofs = 0; my $libs = 0; #> - + my $return_value=0; while () { $line = $_; @@ -678,14 +682,14 @@ sub iterate_proveit_on_libs(){ $go = "ok" if ($from eq $lib); last if $before eq $lib; - if (($go || grep { "$_" eq $lib } @dolist) && + if (($go || grep { "$_" eq $lib } @dolist) && !(grep { "$_" eq $lib } @butlist)) { $libs += 1; if (-d $lib) { $pathlib = $lib; $baselib = ""; - } elsif (-f $lib) { - ($baselib,$pathlib,$typelib) = fileparse($lib,qr{\..*}); + } elsif (-f $lib) { + ($baselib,$pathlib,$typelib) = fileparse($lib,qr{\..*}); $baselib .= $typelib; } else { die "$lib is neither a file nor a directory\n"; @@ -696,7 +700,7 @@ sub iterate_proveit_on_libs(){ $exe =~ s/\%OPTS\%/$opts/g; $command=""; $command .= "$exe"; - + if ($command) { if ($dryrun) { print "DRY-RUN: $command\n"; @@ -725,7 +729,7 @@ sub iterate_proveit_on_libs(){ } print OUTFILE "$proveout\n" if $out; - + my @warnings = ($proveout =~ m/(Warning[:]? .*)/g); if (@warnings) { #< @@ -735,7 +739,7 @@ sub iterate_proveit_on_libs(){ } #> } - + my @errors = ($proveout =~ m/(Error[:]? .*)/g); if (@errors) { $fail_msg = join("\n*** ",@errors); @@ -746,7 +750,7 @@ sub iterate_proveit_on_libs(){ $current_formulas = $1; $current_attempted = $2; $current_proofs = $3; - + $totalformulas += $current_formulas; $totalproofs += $current_proofs; } else { @@ -763,11 +767,11 @@ sub iterate_proveit_on_libs(){ if ($no_color) { print $status; } else { - print DARK RED $status; + print DARK RED $status; } #< my $status_message = ""; - if ( $current_formulas >= 0 ) { + if ( $current_formulas >= 0 ) { my $miss = $current_formulas-$current_attempted; my $unsucc = $current_formulas-$current_proofs; my $comma = ""; @@ -797,7 +801,7 @@ sub iterate_proveit_on_libs(){ # Update my return value $return_value=$fail if ($fail > $return_value); } - + if ($fail == 0) { $status = $ret_val_labels{0}; $status = "OK" if ! $status; @@ -806,7 +810,7 @@ sub iterate_proveit_on_libs(){ if ($no_color) { print $status; } else { - print DARK GREEN $status; + print DARK GREEN $status; } #< $endln = "]\n"; @@ -820,7 +824,7 @@ sub iterate_proveit_on_libs(){ # since warnings are already there. print "*** $warn_msg\n" if $warn_msg && $no_printout; - $depfile = "$lib/pvsbin/$top.dep"; + $depfile = $dir ? "$dir/$lib.dep" : "$lib/$lib.dep"; if (-f $depfile) { open (DEPFILE,"$depfile"); while () { @@ -834,7 +838,7 @@ sub iterate_proveit_on_libs(){ !(grep {$_ eq $deplib} @libraries) && -d $deplib && -f "$deplib/$top.pvs") { print "*** Warning: Library $deplib is out of order. It should appear before $lib in $file\n"; - } + } } else { print "*** Warning: Cannot check library order. Obsolete dep file for library $lib? Try regenerating it.\n"; } @@ -862,7 +866,7 @@ sub iterate_proveit_on_libs(){ my $missed = $totalformulas-$totalproofs; $mssg .= "*** Grand Totals: $totalproofs proofs / $totalformulas formulas. Missed: $missed formulas.\n"; } - $mssg .= "*** Number of libraries: $libs\n"; + $mssg .= "*** Number of libraries: $libs\n"; print $mssg; $summary .= $mssg; #> @@ -902,17 +906,17 @@ die "$file is a directory\n" if -d $file; open (INFILE,$file) || die "File $file not found\n"; if (!$out && !$cleanall && !$clean && !$execute && !$dryrun) { - my ($base,$path,$type) = fileparse($file,qr{\..*}); + my ($base,$path,$type) = fileparse($file,qr{\..*}); $out = "$path$base"; - + my $dol = join('_',@dolist); - $dol =~ s/\//-/g; + $dol =~ s/\//-/g; $out .= "-$dol" if $dol; - + my $butl = join('_',@butlist); - $butl =~ s/\//-/; + $butl =~ s/\//-/; $out .= "-but_$butl" if $butl; - + $out .= "-from_$from" if $from; $out .= "-to_$to" if $to; $out .= "-after_$after" if $after; @@ -923,7 +927,7 @@ if (!$out && !$cleanall && !$clean && !$execute && !$dryrun) { print "PID: $$\n" if ($pid); -if ($out) { +if ($out) { open (OUTFILE,">$out") or print "*** Warnining: cannot create output file $out.\n"; } @@ -946,23 +950,25 @@ $overopts .= " --top \"$top\"" if $top; $overopts .= " --enable \"$enablelist\"" if $enablelist; $overopts .= " --verbose" if $verbose; $overopts .= " --log" if $log; +$overopts .= " --purge" if $purge; $go = "ok" if !($from || $after || @dolist); if ($clearpath) { print "Cleaning PVS_LIBRARY_PATH variable.\n"; $ENV{'PVS_LIBRARY_PATH'}=""; - $addpath=1; + $addpath="" unless defined $addpath; } -if ($addpath) { - $pwd=Cwd::getcwd(); - print "Adding $pwd to PVS_LIBRARY_PATH.\n"; +if (defined $addpath) { + # Empty path means current directory + my $pathto_add = $addpath eq "" ? Cwd::getcwd() : $addpath; + print "Adding $pathto_add to PVS_LIBRARY_PATH.\n"; $pvslibrarypath = $ENV{'PVS_LIBRARY_PATH'}; if ($pvslibrarypath) { - $ENV{'PVS_LIBRARY_PATH'}="$pwd:$pvslibrarypath"; + $ENV{'PVS_LIBRARY_PATH'}="$pathto_add:$pvslibrarypath"; } else { - $ENV{'PVS_LIBRARY_PATH'}="$pwd"; + $ENV{'PVS_LIBRARY_PATH'}="$pathto_add"; } } diff --git a/pvs.in b/pvs.in index 1de627bca..9d6a05119 100755 --- a/pvs.in +++ b/pvs.in @@ -115,6 +115,7 @@ emacsargs= getversion= loadafter= nobg= +noinform= noinit= nowin= opsys=`uname -s` @@ -350,10 +351,12 @@ case $PVSLISP in ALLEGRO_CL_HOME=$PVSPATH/bin/$PVSARCH-$opsys/home noinit="-qq" evalflag="-e" + noinform= ;; sbclisp) noinit="--no-userinit" evalflag="--eval" + noinform="--noinform" ;; esac @@ -389,7 +392,7 @@ if [ -n "${getversion}" ] then export PVSEMACS= export PVS_LIBRARY_PATH= - echo `"${pvsimagepath}" ${noinit} ${evalflag} "(progn(pvs::pvs-version)(terpri)(pvs::exit-pvs))"` + echo `"${pvsimagepath}" ${noinform} ${noinit} ${evalflag} "(progn(pvs::pvs-version)(terpri)(pvs::exit-pvs))"` exit 0 fi @@ -411,7 +414,7 @@ fi # Now run pvs, either through Emacs or the raw PVS image # emacsargs is the arguments not otherwise hendled while processing the command line args if [ -n "${rawmode}" ] # No Emacs involved - PVSEMACS is not set -then "${pvsimagepath}" ${noinit} ${otherargs} +then "${pvsimagepath}" ${noinform} ${noinit} ${otherargs} elif [ -n "${batch}" ] # Emacs, but no windows then ${PVSEMACS} ${batch} ${dotemacs} ${pvsemacsinit} ${emacsargs} ${otherargs} 2>&1 elif [ -n "${nowin}" ] diff --git a/src/Field/README.md b/src/Field/README.md index 8f42e3466..85b89fb1f 100644 --- a/src/Field/README.md +++ b/src/Field/README.md @@ -42,15 +42,25 @@ such as [SLIME](https://slime.common-lisp.dev/) and [SLY](https://joaotavora.git The library includes the following strategy commands, which should be called within the interactive read-eval-loop of the PVS theorem prover. --`(enable-debug-mode [])` and `(disable-debug-mode [])`: -These commands enable/disable, respectively, debug mode, on a list of + +- `(set-debug-mode [] :frames [] :verbose [ none | nil | t ] :mode [ toggle | enable | disable ] :suppress [])`: Configure debug mode. +- `(enable-debug-mode [])` and `(disable-debug-mode [])`: +These commands enable/disable, respectively. Optionally, load a list of Lisp files or directories containing Lisp files. --`(set-debug-mode [] :frames [] :verbose [ none | nil | t ] :mode -[ toggle | enable | disable ] :suppress [])`: -Configure debug mode. -- `(show-debug-mode)`: Print current configuration of debug mode. +- `(show-debug-mode)`: Print current configuration of debug mode. This strategy command +uses the lisp function . +- `(load-files [files] :reset [ nil | t ] :lib [ nil | t ])`: Load files and automatically load them next time this command is used. +Reset memory when `:reset` is `t`. Load them from PVS directory when `:lib` is `t`. ### Lisp Functions +The strategy commands listed above are provided for convience. However, +their are built on the following Lisp functions, which can be directly executed using, for example, the `*pvs*` +interactive buffer. +- `(extra-set-debug-mode ['enable | 'disable] [:files ] [:suppres ])`: Configure debug mode. +- `(extra-show-debug-mode)`: Print current configuration of debug mode. +- `(extra-load-files [FILES | (FILE1 ... FILEn)] [:reset t] [:lib t])`: Load files. + +### Lisp Debugging Functions The Lisp functions `(extra-debug-println ...)`, `(extra-debug-print ...)`, @@ -148,7 +158,7 @@ To print a message "**HERE**", the value of `fnum`, whether `fnum` is positive, ``` (let ((expr (extra-get-formula fnum)) - (dummy (extra-debug-println "**HERE**" + (dummy (extra-debug-println "**HERE**" fnum (> fnum 0) expr (exists-expr? expr)) ...) ``` @@ -347,7 +357,7 @@ ff gg ``` -The command `set-debug-mode` also accepts +The command `set-debug-mode` also accepts the option `:suppress `, where `` is a suppress function. The suppress function is used by by `(extra-debug-print ...)` and `(extra-debug-break ...)` to decide @@ -489,7 +499,7 @@ Loading code instrumented with `extra-debug-print` or `extra-debug-println` with Rule? (mystrat 1) ... %%% -%%% This code requires the feature :extra-debug. To avoid this error at compile time, +%%% This code requires the feature :extra-debug. To avoid this error at compile time, %%% use the conditional compilation directive #+extra-debug before (extra-debug-println ...) %%% (extra-debug-print ...), and (extra-debug-break ...). %%% diff --git a/src/Field/extrategies.lisp b/src/Field/extrategies.lisp index 899122fc5..172610cbe 100644 --- a/src/Field/extrategies.lisp +++ b/src/Field/extrategies.lisp @@ -491,13 +491,13 @@ T, returns NIL when theory is not imported in current theory." theory)))) (defun extra-imported-theory? (theory) - "Find if THEORY is an imported thoery in the current theory. -Return NIL if not." + "Find if THEORY is an imported theory in the current theory (it is assummed that current theory +is always imported in itself). Return NIL if not." (when theory (let ((current-th (current-theory)) (qid (extra-qid-theory theory))) (when current-th - (find qid (all-imported-theories current-th) + (find qid (cons current-th (all-imported-theories current-th)) :test (lambda (qid th) (string= qid (extra-qid-theory th)))))))) (defun extra-qid-theory (theory) @@ -3574,7 +3574,8 @@ when the list of FNUMS is over. Options are as in eval-formula." (unbound-variable (c) (when *extra-debug-verbose* - (format t "[suppress-when] Variable ~a is unbound in ~a. Expression assumed not to hold~%" (cell-error-name c) expr)))))))) + (format t "[suppress-when] Variable ~a is unbound in ~a. Expression assumed not to hold~%" + (cell-error-name c) expr)))))))) (setf (documentation fun 'function) (format nil "when expression ~a holds" expr)) fun)) @@ -3591,7 +3592,8 @@ when the list of FNUMS is over. Options are as in eval-formula." (c) (not (when *extra-debug-verbose* - (format t "[suppress-unless] Variable ~a is unbound in ~a. Expression assummed not to hold~%" (cell-error-name c) expr))))))))) + (format t "[suppress-unless] Variable ~a is unbound in ~a. Expression assummed not to hold~%" + (cell-error-name c) expr))))))))) (setf (documentation fun 'function) (format nil "unless expression ~a holds" expr)) fun)) @@ -3700,9 +3702,8 @@ string, it prints the the string resulting from evaluating (format nil = , where is the evaluation of . In addition, this function will print backtrace frames (according to global variable *extra-debug-frame-count* and status of strategies stack at the point where the functions is -called. Compiling a call of this function through (extra-set-debug-mode ...) without enabling debug mode -results in a compilation error. This compilation error could be avoided by adding the compilation -directive #+extra-debug before the call to the function." +called. Compiling a call of this function without enabling debug mode results in a compilation error. +This compilation error could be avoided by adding the compilation directive #+extra-debug before the call to the function." `(extra-debug-aux "*extra-debug-print*" ,data)) (defmacro extra-debug-break (&rest data) @@ -3716,15 +3717,15 @@ extra-debug-print. Data is a list of either a string, a formatted string of the If the i-th data input is a string, it prints the string.If the i-th data input is formatted string, it prints the the string resulting from evaluating (format nil ... ). Otherwise, when the i-th data input is a Lisp expression EXPR, it prints the line = , where -is the evaluation of . Compiling a call of this function without enabling debug mode through -(extra-set-debug-mode ...) results in a compilation error. This compilation error could be avoided by adding -the compilation directive #+extra-debug before the call to the function." +is the evaluation of . Compiling a call of this function without enabling debug mode results +in a compilation error. This compilation error could be avoided by adding the compilation +directive #+extra-debug before the call to the function." (unless (member :extra-debug *features*) (error *debug-fail-msg*)) `(format t "~%[*extra-debug-println*] ~{~a~@[ = ~{~s~}~]~^, ~}~%" (extra-debug-data ,data))) -(defun extra-show-debug-mode (&optional msgs) +(defun extra-show-debug-mode__ (&optional msgs) (format nil "~&*extra-debug-frame-count*: ~a~ ~%*extra-debug-files*: ~a~ ~%*extra-debug-verbose*: ~a~ @@ -3735,8 +3736,12 @@ the compilation directive #+extra-debug before the call to the function." (documentation *extra-debug-suppress* 'function) (member :extra-debug *features*) msgs)) +(defun extra-show-debug-mode () + "[Extrategies] Show current debug mode." + (format t (extra-show-debug-mode__))) + (defstrat show-debug-mode () - (let ((msg (extra-show-debug-mode))) + (let ((msg (extra-show-debug-mode__))) (printf "~a" msg)) "[Extrategies] Show current debug mode.") @@ -3802,10 +3807,38 @@ previously in *extra-debug-files*. When :LIB is t, it treats the file names in F PVS home directory or to any directory in the PVS Library Path." (let ((loaded-notfound (extra-load-files__ files reset lib))) (when loaded-notfound - (format t "~@[~%Loaded files: ~{~a~^, ~}~]~@[~%Files not found: ~{~a~^, ~}~]" + (format t "~%~@[~%Loaded files: ~{~a~^, ~}~]~@[~%Files not found: ~{~a~^, ~}~]" (car loaded-notfound) (cdr loaded-notfound))))) ;; See set-debug mode +(defun extra-set-debug-mode__ (mode &key files frames (verbose 'none) suppress) + (let ((msgs)) + (unless (equal verbose 'none) + (setq *extra-debug-verbose* (when verbose t))) + (cond ((eq mode 'toggle) + (if (member :extra-debug *features*) + (setq *features* (delete :extra-debug *features*)) + (pushnew :extra-debug *features*))) + ((eq mode 'enable) + (pushnew :extra-debug *features*)) + ((eq mode 'disable) + (setq *features* (delete :extra-debug *features*))) + (mode (push "MODE should be one of toggle, enable, or disable" msgs))) + (when frames + (if (numberp frames) + (setq *extra-debug-frame-count* frames) + (push (format nil "FRAMES (~a) must be a number" frames) msgs))) + (when suppress + (let ((fsuppress (eval suppress))) + (if (typep fsuppress 'function) + (setq *extra-debug-suppress* fsuppress) + (push (format nil "SUPPRESS (~a) must be a function" suppress) msgs)))) + (when files + (let ((notfound (cdr (extra-load-files__ files t nil)))) + (when notfound (format nil "Files not found: ~{~s~^, ~}" notfound)))) + (extra-show-debug-mode__ msgs))) + + (defun extra-set-debug-mode (&optional mode &key files frames (verbose 'none) suppress) "[Extrategies] Load files or directories specified in FILES afer enabling/disabling debug mode. In the case of directories, load all files *.pvs, pvs-attachments, and pvs-strategies in the directory. @@ -3854,33 +3887,10 @@ TECHNICAL NOTES: - EXPR in (suppress-when EXPR) and (suppress-unless EXPR) can be an arbitrary Lisp code including global variables, variables that are printed by extra-debug-print and extra-debug-break, and tags that are specified by those functions." - (let ((msgs)) - (unless (equal verbose 'none) - (setq *extra-debug-verbose* (when verbose t))) - (cond ((eq mode 'toggle) - (extra-set-debug-mode - (if (member :extra-debug *features*) 'disable 'enable) :files files :frames frames :verbose verbose)) - ((eq mode 'enable) - (pushnew :extra-debug *features*)) - ((eq mode 'disable) - (setq *features* (delete :extra-debug *features*))) - (mode (push "MODE should be one of toggle, enable, or disable" msgs))) - (when frames - (if (numberp frames) - (setq *extra-debug-frame-count* frames) - (push (format nil "FRAMES (~a) must be a number" frames) msgs))) - (when suppress - (let ((fsuppress (eval suppress))) - (if (typep fsuppress 'function) - (setq *extra-debug-suppress* fsuppress) - (push (format nil "SUPPRESS (~a) must be a function" suppress) msgs)))) - (when files - (let ((notfound (cdr (extra-load-files__ files t nil)))) - (when notfound (format nil "Files not found: ~{~s~^, ~}" notfound)))) - (extra-show-debug-mode msgs))) + (format t (extra-set-debug-mode__ mode :files files :frames frames :verbose verbose :suppress suppress))) (defstrat set-debug-mode (&key mode frames (verbose none) suppress &rest files) - (let ((msg (extra-set-debug-mode mode :files files :frames frames :verbose verbose :suppress suppress))) + (let ((msg (extra-set-debug-mode__ mode :files files :frames frames :verbose verbose :suppress suppress))) (printf "~a" msg)) "[Extrategies] Load files or directories specified in FILES afer enabling/disabling debug mode. In the case of directories, load all files *.pvs, pvs-attachments, and pvs-strategies in the directory. @@ -3932,14 +3942,14 @@ TECHNICAL NOTES: ") (defstrat enable-debug-mode (&rest files) - (let ((msg (extra-set-debug-mode 'enable :files (or files *extra-debug-files*)))) + (let ((msg (extra-set-debug-mode__ 'enable :files (or files *extra-debug-files*)))) (printf "~a" msg)) "[Extrategies] Load files or directories specified in FILES afer enabling debug mode. In the case of directories, load all files *.pvs, pvs-attachments, and pvs-strategies in the directory. If FILES is null, load files in *extra-debug-files*.") (defstrat disable-debug-mode (&rest files) - (let ((msg (extra-set-debug-mode 'disable :files (or files *extra-debug-files*)))) + (let ((msg (extra-set-debug-mode__ 'disable :files (or files *extra-debug-files*)))) (printf "~a" msg)) "[Extrategies] Load files or directories specified in FILES afer disabling debug mode. In the case of directories, load all files *.pvs, pvs-attachments, and pvs-strategies in the directory. diff --git a/src/PVSio/pvs-lib.lisp b/src/PVSio/pvs-lib.lisp index ec61ed1ca..37e202d11 100644 --- a/src/PVSio/pvs-lib.lisp +++ b/src/PVSio/pvs-lib.lisp @@ -102,7 +102,7 @@ Assume loadedfile is not null and there is not theory with theoryid in current c (defun load-pvs-attachment (file &optional force (verbose t)) "Load file containing PVS attachment. FILE is provided as an absolute path, e.g., -using make-pathname or merge-pathnames." +using probe-file, make-pathname or merge-pathnames." (let ((source (probe-file file))) (when source (let ((outdated-src (outdated-sourcefile source))) diff --git a/src/ProofLite/proveit-init.lisp b/src/ProofLite/proveit-init.lisp index 1ac1106d1..d22cc99bd 100644 --- a/src/ProofLite/proveit-init.lisp +++ b/src/ProofLite/proveit-init.lisp @@ -20,7 +20,7 @@ (car thf)))) ;; Split string given a character -(defun split (str char) +(defun split (str char) (when str (let ((pos (position char str))) (if pos @@ -30,7 +30,7 @@ (list str))))) ;; Converts a string "th.f1:..:fn into a list ("th" "f1" ... "fn"), -(defun thf2list (thf) +(defun thf2list (thf) (let* ((l (split thf #\.))) (cons (car l) (split (cadr l) #\:)))) @@ -51,7 +51,7 @@ ;; that is alpabethically ordered and where formulas of the same theory are ;; put together (theories without formulas are removed) (defun thfs2list (thsf) - (let* ((l (sort (remove-if-not + (let* ((l (sort (remove-if-not #'cdr (mapcar #'thf2list thsf)) #'string<= :key #'car))) @@ -137,7 +137,7 @@ (idlength reporter) decl-id proof-status - decision-procedure + decision-procedure (if time (format nil "~v,2f" (timelength reporter) time) (format nil "~v" (timelength reporter)))))) @@ -190,11 +190,11 @@ (defun get-obfuscated-path (pathname) "To address security concerns, a pathname gets obfuscated by replacing - know library paths by collection Ids, the home path by '$HOME', and + know library paths by collection Ids, the home path by '$HOME', and the pvs path by '$PVS_DIR'." (let*((dir-names (cdr (pathname-directory pathname))) (collection-id - (when (fboundp 'extra-get-pvslib-id-from-dir) + (when (fboundp 'extra-get-pvslib-id-from-dir) (extra-get-pvslib-id-from-dir (format nil "~{/~a~}/" (subseq dir-names 0 (max 0 (- (length dir-names) 1)))))))) (if collection-id @@ -204,7 +204,7 @@ (substitute #\- #\/ collection-id) (last dir-names)) (let ((collection-id - (when (fboundp 'extra-get-pvslib-id-from-dir) + (when (fboundp 'extra-get-pvslib-id-from-dir) (extra-get-pvslib-id-from-dir (directory-namestring pathname))))) (if collection-id (format nil "~a/~a" (substitute #\- #\/ collection-id) (file-namestring pathname)) @@ -238,7 +238,7 @@ (format stream "~%## Platform information ~%") (format stream "~&| | |~%|---|---|~%" ) (format stream "~&| Machine Info | **~a** (~a - ~a - ~a ~a) |~%" (machine-instance) (machine-type) (machine-version) (software-type) (software-version)) - (format stream "~&| PVS | ~a (~a) |~%" + (format stream "~&| PVS | ~a (~a) |~%" (get-pvs-version) (let ((git-info (when (git-available-p) (git-current-branch)))) (or git-info "no git info available"))) @@ -283,7 +283,7 @@ ((string= proof-status "untried") "✴") ((prefix? "proved" proof-status) "✅")) proof-status - decision-procedure + decision-procedure (if time (secs->ddhhmmss time) "n/a")))) @@ -342,7 +342,7 @@ (format stream "Run started at ~a.~%~%" (starting-time reporter)) (format stream "~& PVS Version , ~a ~%" (get-pvs-version)) (format stream "~& Lisp, ~a ~a ~%" (lisp-implementation-type) (lisp-implementation-version)) - (format stream "~& Patch Version, ~a ~%" (or (get-patch-version) "n/a")) + (format stream "~& Patch Version, ~a ~%" (or (get-patch-version) "n/a")) (format stream "~& Library Path ~{, \"~a\"~^, ~%~} ~%" *pvs-library-path*) (format stream "~& Loaded Patches~{, \"~a\"~^, ~%~} ~%" *pvs-patches-loaded*)) (with-open-file @@ -354,7 +354,7 @@ tot attempted proved missing (secs->ddhhmmss time))) (loop for cont in (grand-table reporter) when cont do (format stream cont))) (with-open-file - (stream (format nil "~a/~a" (dir reporter) (detailed-filename reporter)) :direction :output :if-exists :supersede) + (stream (format nil "~a/~a" (dir reporter) (detailed-filename reporter)) :direction :output :if-exists :supersede) (loop for cont in (content reporter) when cont do (format stream cont)) ;; )) @@ -383,7 +383,7 @@ "~&~a, ~a, ~a, ~a~%" decl-id proof-status - decision-procedure + decision-procedure (if time (secs->ddhhmmss time) "n/a")))) @@ -421,13 +421,13 @@ "Proof-status reporters (by default, the classic mode is on)") (defun proveit-status-proof-theories (theories thfs) - #+pvsdebug (format t "~%[proveit-init.proveit-status-proof-theories] theories ~a thfs ~a ~%" theories thfs) + #+pvsdebug (format t "~%[proveit-init.proveit-status-proof-theories] theories ~a thfs ~a ~%" theories thfs) (let ((return-value 0)) (if theories (let ((*disable-gc-printout* t)) (pvs-buffer "PVS Status" (with-output-to-string - (*standard-output*) + (*standard-output*) (multiple-value-bind (tot proved unfin untried time) (proveit-proof-summaries theories thfs) @@ -439,7 +439,7 @@ return-value)) (defun proveit-proof-summaries (theory-ids thfs - &optional filename) + &optional filename) (let ((tot 0) (proved 0) (unfin 0) (untried 0) (time 0)) #+pvsdebug (format t "~&[proveit-init.proveit-proof-summaries] ~%") (dolist (reporter *proof-status-reporters*) @@ -466,14 +466,14 @@ (typechecked? theory)) (let* ((fdecls (provable-formulas theory))) (dolist (decl fdecls) - (let ((dof (member (format nil "~a" (id decl)) (cdr thf) + (let ((dof (member (format nil "~a" (id decl)) (cdr thf) :test #'string=))) (when (or (null thf) dof) (let ((tm (if (run-proof-time decl) (/ (run-proof-time decl) - internal-time-units-per-second 1.0) + internal-time-units-per-second 1.0) 0))) - (incf tot) + (incf tot) (cond ((proved? decl) (incf proved)) ((justification decl) (incf unfin)) @@ -511,7 +511,7 @@ ;; ;; -(defun proveit-theories (theories retry? thfs +(defun proveit-theories (theories retry? thfs &optional txtproofs texproofs use-default-dp? save-proofs?) (let ((*use-default-dp?* use-default-dp?)) (read-strategies-files) @@ -519,23 +519,23 @@ (with-context theory (let ((thf (car (member theory thfs :test #'eq-thf))) (main-filename (format nil "~a.proofs" (id theory)))) - (if (null thf) + (if (null thf) (pvs-message "Proving theory ~a" (id theory)) - (pvs-message "Proving formulas ~a in theory ~a" + (pvs-message "Proving formulas ~a in theory ~a" (cdr thf) (id theory))) (when texproofs (let ((main-filename (format nil "pvstex/~a.tex" main-filename))) (when (probe-file main-filename) (delete-file main-filename)))) (let ((*justifications-changed?* nil)) (dolist (decl (provable-formulas theory)) - (let ((dof (member (format nil "~a" (id decl)) (cdr thf) + (let ((dof (member (format nil "~a" (id decl)) (cdr thf) :test #'string=))) (when (or (null thf) dof) (setq *last-proof* (pvs-prove-decl decl retry?)) (when txtproofs - (with-open-file + (with-open-file (*standard-output* - (ensure-directories-exist + (ensure-directories-exist (pathname (format nil "pvstxt/~a.txt" (id decl)))) :direction :output :if-does-not-exist :create @@ -551,7 +551,7 @@ ;; (defun now-today () - (multiple-value-bind (s mi h d mo y dow dst tz) + (multiple-value-bind (s mi h d mo y dow dst tz) (get-decoded-time) (declare (ignore tz dst dow)) (format nil "~a:~a:~a ~a/~a/~a" h mi s mo d y))) @@ -563,7 +563,7 @@ no id can be found for the directory ''/Users/username/pvs/nasalib/'." (let*((dir-names (cdr (pathname-directory pathname))) (collection-id - (when (fboundp 'extra-get-pvslib-id-from-dir) + (when (fboundp 'extra-get-pvslib-id-from-dir) (extra-get-pvslib-id-from-dir (format nil "~{/~a~}/" (subseq dir-names 0 (max 0 (- (length dir-names) 1)))))))) (if collection-id @@ -594,7 +594,8 @@ context proveitarg pvsfile import scripts write-scripts traces force autotop typecheckonly txtproofs texproofs preludext disabled-oracles enabled-oracles auto-fix? default-proof thfs theories - dependencies alternative-summary-modes debug-mode-on? outdir outbasename) + dependencies depfile alternative-summary-modes debug-mode-on? outdir outbasename + purge?) (let* ((*print-readably* nil) (*noninteractive* t) (*pvs-verbose* (if traces 3 2)) @@ -637,7 +638,7 @@ (grand-totals-filename md-reporter) (detailed-filename md-reporter) (run-report-filename md-reporter)))) - (format t "~%*** ~%*** Processing ~a (~a)~%*** Generated by ~a~%" + (format t "~%*** ~%*** Processing ~a (~a)~%*** Generated by ~a~%" proveitarg current-timestamp proveitversion) ;; auto-fix (when (and auto-fix? (numberp auto-fix?)) @@ -649,7 +650,7 @@ (format t "*** Using default proof for open branches: ~a~%" default-proof)) (extra-disable-oracles disabled-oracles enabled-oracles) (let ((orcls (extra-list-oracles))) - (when orcls + (when orcls (format t "*** Trusted Oracles~%") (loop for orcl in orcls do (format t "*** ~a: ~a~%" @@ -665,7 +666,7 @@ (top-already-exists (cnd) (format t "~%*** Warning: ~a. Omitting generation.~%" (format nil "~a" cnd))))) #+pvsdebug (format t "~&[proveit-init.proveit] after autotop checkpoint~%") - (when pvsfile + (when pvsfile (let ((*pvs-error-hook* (lambda (msg err buff place) (declare (ignore buff place)) @@ -675,10 +676,9 @@ #+pvsdebug (format t "~&[proveit-init.proveit] after typecheck checkpoint~%") (save-context) (let* ((theory-names (or theories (and pvsfile (theories-in-file pvsfile)))) - (pvstheories + (pvstheories (if import (imported-theories-in-theories theory-names) - (mapcar #'get-typechecked-theory theory-names))) - (depfile (pathname (format nil "pvsbin/~a.dep" (or pvsfile "bot"))))) + (mapcar #'get-typechecked-theory theory-names)))) ;; check unreachable theories #+pvsdebug (format t "~%[proveit-init.proveit] pvsfile ~a import ~a~%" pvsfile import) (when (and (string= pvsfile "top") import) @@ -688,22 +688,22 @@ (loop for th being the hash-values of (pvs-theories (current-workspace)) collect (filename th))) (missing-files (set-difference files-in-dir reachable-files :test #'string=))) - #+pvsdebug (format t "~%[proveit-init.proveit] files-in-dir ~{~a ~}~%" files-in-dir) - #+pvsdebug (format t "~%[proveit-init.proveit] reachable-files ~{~a ~}~%" reachable-files) - #+pvsdebug (format t "~%[proveit-init.proveit] missing-files ~{~a ~}~%" missing-files) + #+pvsdebug (format t "~%[proveit-init.proveit] files-in-dir ~{~a ~}~%" files-in-dir) + #+pvsdebug (format t "~%[proveit-init.proveit] reachable-files ~{~a ~}~%" reachable-files) + #+pvsdebug (format t "~%[proveit-init.proveit] missing-files ~{~a ~}~%" missing-files) (when missing-files (let ((*disable-gc-printout* t)) (let ((plural? (< 1 (length missing-files)))) (format t "~&*** Warning: file~:[~;s~] ~{~#[~;~a.pvs~;~a.pvs and ~a.pvs~:;~@{~a.pvs~#[~;, and ~:;, ~]~}~]~} ~:[is~;are~] not reachable from top.pvs~%" plural? missing-files plural?)))))) ;; dependencies - (unless (equal dependencies "nil") - (let((relative-path-lib-names? (equal dependencies "relative"))) - (with-open-file - (stream (ensure-directories-exist depfile) + (unless (string= dependencies "") + (let((relative-path-lib-names? (string= dependencies "relative"))) + (with-open-file + (stream (ensure-directories-exist depfile) :direction :output :if-exists :supersede :if-does-not-exist :create) - (format stream + (format stream "~{~a~^,~}~%" (mapcar #'(lambda (th) (qualified-th-name th relative-path-lib-names?)) @@ -721,13 +721,13 @@ for idth = (id th) do (format stream "~a:~{~a~^,~}~%" (qualified-th-name th relative-path-lib-names?) (mapcar - #'(lambda(x) + #'(lambda(x) (if (lib-datatype-or-theory? x) (format nil "~a" (qualified-th-name x relative-path-lib-names?)) (qualified-th-name x relative-path-lib-names?))) (immediate-theories-in-theory idth))))))) - (let ((pvstheories + (let ((pvstheories (remove-if #'(lambda (th) (typep th '(or datatype codatatype))) pvstheories))) (if typecheckonly @@ -745,26 +745,35 @@ prl-filename (id theory)) (install-prooflite-scripts-from-prl-file theory prlfile force)) (install-prooflite-scripts (filename theory) (id theory) 0 force)))) - #+pvsdebug (format t "~%[proveit-init.proveit] before proveit-theories~%") + #+pvsdebug (format t "~%[proveit-init.proveit] before proveit-theories~%") (proveit-theories pvstheories force thfs txtproofs texproofs nil ;; if auto-fix?, save proofs auto-fix?) (setq proveit-return-value - (proveit-status-proof-theories pvstheories thfs)))) + (proveit-status-proof-theories pvstheories thfs)) + (when purge? + (dolist (theory pvstheories) + (purge-proved-formulas-file (filename theory)))))) (save-context) (when write-scripts (dolist (theory pvstheories) (write-all-prooflite-scripts-to-file (format nil "~a" (id theory))))))) #+pvsdebug (format t "~&[proveit-init.proveit] proveit-return-value ~a~%" proveit-return-value) - (bye proveit-return-value)))) + (bye proveit-return-value)))) (defun proveit () - (let* ((proveitversion + (let* ((proveitversion (or (environment-variable "PROVEITVERSION") (format nil "proveit ~a" *prooflite-version*))) (context (environment-variable "PROVEITPVSCONTEXT")) (proveitarg (environment-variable "PROVEITARG")) - (pvsfile (let ((name (environment-variable "PROVEITPVSFILE"))) + (pvsfile (let ((name (environment-variable "PROVEITPVSFILENAME"))) (when (and name (string/= name "")) name))) + (outdir (let ((name (environment-variable "PROVEITOUTDIR"))) + (when (and name (string/= name "")) name))) + (outbasename (let ((name (environment-variable "PROVEITOUTBASENAME"))) + (when (and name (string/= name "")) name))) + (dependencies (environment-variable "PROVEITDEPENDENCIES")) + (depfile (environment-variable "PROVEITDEPFILE")) (import (read-from-environment-variable "PROVEITLISPIMPORT")) (scripts (read-from-environment-variable "PROVEITLISPSCRIPTS")) (write-scripts (read-from-environment-variable "PROVEITLISPWRITESCRIPTS")) @@ -777,7 +786,7 @@ (preludext (remove-duplicates (read-from-environment-variable "PROVEITLISPPRELUDEXT") :test #'string=)) - (disabled-oracles (remove-duplicates + (disabled-oracles (remove-duplicates (read-from-environment-variable "PROVEITLISPDISABLE") :test #'string=)) (enabled-oracles (remove-duplicates @@ -785,25 +794,22 @@ :test #'string=)) (auto-fix? (read-from-environment-variable "PROVEITLISPAUTOFIX")) (default-proof (let ((envstr (environment-variable - "PROVEITLISPDEFAULTPROOFSCRIPT"))) + "PROVEITLISPDEFAULTPROOFSTEP"))) (when envstr (read-from-string envstr)))) (thfs (thfs2list (read-from-environment-variable "PROVEITLISPTHFS"))) (theories (remove-duplicates (read-from-environment-variable "PROVEITLISPTHEORIES") :test #'string=)) - (dependencies (environment-variable "PROVEITLISPDEPENDENCIES")) (alternative-summary-modes (remove-duplicates (read-from-environment-variable "PROVEITLISPALTSUMMARIESMODE") :test #'string=)) (debug-mode-on? (environment-variable "DEBUG")) - (outdir (let ((name (environment-variable "PROVEITLISPOUTDIR"))) - (when (and name (string/= name "")) name))) - (outbasename (let ((name (environment-variable "PROVEITLISPOUTBASENAME"))) - (when (and name (string/= name "")) name)))) + (purge? (read-from-environment-variable "PROVEITLISPPURGE"))) (proveit-on proveitversion context proveitarg pvsfile import scripts write-scripts traces force autotop typecheckonly txtproofs texproofs preludext disabled-oracles enabled-oracles auto-fix? default-proof thfs theories - dependencies alternative-summary-modes debug-mode-on? outdir outbasename))) + dependencies depfile alternative-summary-modes debug-mode-on? outdir outbasename + purge?))) (defun collect-top-theories () (let ((files-in-dir @@ -819,7 +825,7 @@ do (loop for th in theories-in-file do (module-hierarchy* th nil)) append (delete-if #'generated-by theories-in-file)))) - (loop for th being the hash-keys of *modules-visited* + (loop for th being the hash-keys of *modules-visited* for used-ths = (gethash th *modules-visited*) unless (generated-by th) do (setq theories-in-dir (set-difference theories-in-dir used-ths))) diff --git a/src/context.lisp b/src/context.lisp index b190044b6..0068d05b8 100644 --- a/src/context.lisp +++ b/src/context.lisp @@ -1,11 +1,6 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -*- Mode: Lisp -*- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; context.lisp -- Context structures and accessors ;; Author : Sam Owre -;; Created On : Fri Oct 29 19:09:32 1993 -;; Last Modified By: Sam Owre -;; Last Modified On: Sun May 28 19:14:47 1995 -;; Update Count : 69 -;; Status : Stable ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -------------------------------------------------------------------- @@ -1752,7 +1747,7 @@ Note that this doesn't check if the .pvs file is the matches as well." `(("proof-id" . ,(string (car prf))) ("description" . ,(cadr prf)) ("create-date" . ,(caddr prf)) - ("script" . ,(format nil "~s" (cadddr prf))) + ("script" . ,(sformat "~s" (cadddr prf))) ("refers-to" . ,(mapcar #'proof-decl-ref-alist (car (cddddr prf)))))) (defun proof-decl-ref-alist (decl-ref) @@ -3374,36 +3369,154 @@ each context, the theories are in alphabetic order." (t (format t "~%Theory ~a not found, ignoring" theoryid))) (restore-proofs-from-split-file* input prfpath))))) +;; Begin fix for cleanup-proofs-pvs-file + +;;; Fix for cleanup-proofs-pvs-file +;;; +;;; The original implementation has a bug: read-pvs-file-proofs converts the +;;; file format (11-element proofs) to an internal format (6-element proofs), +;;; but cleanup-proofs-pvs-file then writes this internal format back to the file. +;;; This creates malformed .prf files that fail with "(SYMBOLP ID) failed". +;;; +;;; The fix is to read the raw file format without conversion, then filter it. + +(defun read-raw-pvs-file-proofs (filename &optional (dir *default-pathname-defaults*)) + "Read proof file without converting to internal format" + (let ((prf-file (make-prf-pathname filename dir))) + (if (uiop:file-exists-p prf-file) + (handler-case + (with-open-file (input prf-file :direction :input) + (read-proof-file-stream input)) + (error (condition) + (pvs-message "Error reading proof file ~a:~% ~a" + (namestring prf-file) condition) + nil)) + (pvs-message "Proof file ~a does not exist" prf-file)))) + (defun cleanup-proofs-pvs-file (file) - (let* ((aproofs (read-pvs-file-proofs file)) - (dproofs (collect-default-proofs aproofs))) + "Remove non-default proofs from a .prf file" + (let* ((aproofs (read-raw-pvs-file-proofs file)) + (dproofs (collect-default-proofs-raw aproofs))) (if (equalp aproofs dproofs) - (pvs-message "Proof file is already cleaned up") - (let* ((prf-file (make-prf-pathname file)) - (prf-fstr (namestring prf-file)) - (prf-bak (concatenate 'string prf-fstr ".bak"))) - (pvs-message "Moving ~a to ~a" prf-file prf-bak) - (rename-file prf-file prf-bak) - (pvs-message "Writing cleaned up proof file ~a" prf-file) - (multiple-value-bind (value condition) - (ignore-file-errors - (with-open-file (out prf-file :direction :output - :if-exists :supersede) - (mapc #'(lambda (prf) - (write prf :length nil :level nil :escape t - :pretty *save-proofs-pretty* - :stream out) - (when *save-proofs-pretty* (terpri out))) - dproofs) - (terpri out))) - (declare (ignore value)) - (if (or condition - (setq condition - (and *validate-saved-proofs* - (invalid-proof-file prf-file dproofs)))) - (pvs-message "Error writing out proof file:~% ~a" - condition) - (pvs-message "Proof file ~a written" prf-file))))))) + (pvs-message "Proof file is already cleaned up") + (let* ((prf-file (make-prf-pathname file)) + (prf-fstr (namestring prf-file)) + (prf-bak (concatenate 'string prf-fstr ".bak"))) + (pvs-message "Moving ~a to ~a" prf-file prf-bak) + (rename-file prf-file prf-bak) + (pvs-message "Writing cleaned up proof file ~a" prf-file) + (multiple-value-bind (value condition) + (ignore-file-errors + (with-open-file (out prf-file :direction :output + :if-exists :supersede) + (mapc #'(lambda (prf) + (write prf :length nil :level nil :escape t + :pretty *save-proofs-pretty* + :stream out) + (when *save-proofs-pretty* (terpri out))) + dproofs) + (terpri out))) + (declare (ignore value)) + (if (or condition + (setq condition + (and *validate-saved-proofs* + (invalid-proof-file prf-file dproofs)))) + (pvs-message "Error writing out proof file:~% ~a" + condition) + (pvs-message "Proof file ~a written" prf-file))))))) + +(defun collect-default-proofs-raw (proofs) + "Collect only default proofs from raw proof structure" + (mapcar #'collect-theory-default-proofs-raw proofs)) + +(defun collect-theory-default-proofs-raw (proofs) + "Process one theory's proofs" + (cons (car proofs) ;; theory id + (mapcar #'collect-formula-default-proofs-raw (cdr proofs)))) + +(defun collect-formula-default-proofs-raw (proofs) + "Keep only the default proof for a formula. + Input format: (formula-id index proof1 proof2 ...) + Output format: (formula-id 0 default-proof)" + (let* ((index (cadr proofs)) + (all-proofs (cddr proofs)) + (default-proof (nth index all-proofs))) + (list (car proofs) ;; formula id + 0 ;; new index (always 0 now) + default-proof))) + +;; End fix cleanup-proofs-pvs-file + +;;; ============================================================================ +;;; Purge non-default proofs for a single formula (if default is proved) +;;; ============================================================================ + +(defun purge-formula-proofs (theoryref formularef &optional (save? t)) + "Remove non-default proofs from a formula if its default proof status is 'proved'. + THEORYREF: theory name (string) + FORMULAREF: formula name (string) + SAVE?: if T, save the proof file after purging (default T) + Returns T if proofs were purged, NIL otherwise. + Uses find-formula from prooflite.lisp" + (let ((formula (find-formula theoryref formularef))) + (cond + ((null formula) + (pvs-message "Formula ~a not found in theory ~a" formularef theoryref) + nil) + ((not (eq (proof-status formula) 'proved)) + (pvs-message "Formula ~a is not proved (status: ~a)" + formularef (proof-status formula)) + nil) + ((<= (length (proofs formula)) 1) + (pvs-message "Formula ~a has only ~a proof(s), nothing to purge" + formularef (length (proofs formula))) + nil) + (t + (purge-formula-proofs* formula save?))))) + +(defun purge-formula-proofs* (formula &optional save?) + "Actually purge the non-default proofs from FORMULA. + SAVE?: if T, save the proof file after purging" + (let* ((default (default-proof formula)) + (num-before (length (proofs formula)))) + ;; Keep only the default proof + (setf (proofs formula) (list default)) + ;; Update the proof file if requested + (when save? + (let ((file (filename (module formula)))) + (save-pvs-file-proofs file t))) ;; force save + (pvs-message "Purged ~a non-default proof(s) from ~a (kept: ~a)" + (1- num-before) (id formula) (id default)) + t)) + +(defun purge-proved-formulas-file (filename &optional (dir *default-pathname-defaults*)) + "Purge non-default proofs from all proved formulas in a file. + FILENAME: pvs/prf file name + Returns the number of formulas purged." + (let ((prf-file (make-prf-pathname filename dir))) + (unless (uiop:file-exists-p prf-file) + (pvs-message "Proof file ~a does not exist" prf-file) + (return-from purge-proved-formulas-file nil)) + (with-pvs-file + (file) prf-file + (let ((theories (cdr (gethash file (current-pvs-files)))) + (count 0)) + (dolist (th theories) + (let ((theory (get-theory th))) + (when theory + (dolist (decl (append (assuming theory) + (when (module? theory) (theory theory)))) + (when (and (formula-decl? decl) + (eq (proof-status decl) 'proved) + (> (length (proofs decl)) 1)) + (purge-formula-proofs* decl nil) ;; don't save yet + (incf count)))))) + (when (> count 0) + (save-pvs-file-proofs file t)) ;; save once at the end + (if (zerop count) + (pvs-message "No formulas needed purging in ~a" file) + (pvs-message "Purged proofs from ~a formula(s) in ~a" count file)) + count)))) (defun collect-default-proofs (proofs) (mapcar #'collect-theory-default-proofs proofs)) diff --git a/src/datatype.lisp b/src/datatype.lisp index 033b4aa34..91ce915fe 100644 --- a/src/datatype.lisp +++ b/src/datatype.lisp @@ -235,7 +235,7 @@ generated") (pvs-message "Error in writing out ~a: ~a" (namestring adt-path) condition) (pvs-message "Wrote pvs file ~a" adt-file))) - (chmod "a-w" (namestring adt-path))) + (ignore-errors (chmod "a-w" (namestring adt-path)))) ;; (assert (and #+allegro (file-exists-p adt-path) ;; #-allegro (probe-file adt-path) ;; (get-context-file-entry (filename adt)) diff --git a/src/interface/pvs-emacs.lisp b/src/interface/pvs-emacs.lisp index e7e652f55..e72166494 100644 --- a/src/interface/pvs-emacs.lisp +++ b/src/interface/pvs-emacs.lisp @@ -1,11 +1,6 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -*- Mode: Lisp -*- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; pvs-emacs.lisp -- ;; Author : Sam Owre -;; Created On : Thu Dec 16 02:42:01 1993 -;; Last Modified By: Sam Owre -;; Last Modified On: Mon Dec 17 01:30:40 2012 -;; Update Count : 23 -;; Status : Stable ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -------------------------------------------------------------------- @@ -75,6 +70,15 @@ (restore) (pvs-abort))))))) +(defun break-but-ignore-as-error () + "Used by Emacs validate to purposely cause a break, but not treat it as an error +Needed when we want to test how things work in a break." + (handler-case (error "Breaking on purpose for the test") + (error (cnd) + ;; Make sure IGNORE-ERR is printed befoe the break + (format t "IGNORE-ERR") + (break (format nil "~a" cnd))))) + #+(or akcl harlequin-common-lisp) (defmacro pvs-errors (form) "Handle errors when evaluating FORM." diff --git a/src/interface/pvs-json-methods.lisp b/src/interface/pvs-json-methods.lisp index d957eed45..d4ef69b78 100644 --- a/src/interface/pvs-json-methods.lisp +++ b/src/interface/pvs-json-methods.lisp @@ -26,6 +26,10 @@ "List methods clients need to support" (list "info" "warning" "debug" "buffer" "yes-no" "dialog")) +(defrequest pvs-meta-info () + "Get PVS setup/configuration/installation information" + (pvs:pvs-meta-info)) + (defrequest help (methodname) "Get help for the specified methodname - provides the docstring and the argument spec" @@ -550,17 +554,35 @@ to the associated declaration." (declare (ignore containing-terms)) ; might be useful later (json-term term)))) -(defun pvs2alist-proof (proof) +(defun print-timestamp-as-iso (timestamp) + (when timestamp + (multiple-value-bind + (second minute hour date month year day-of-week dst-p tz) + (decode-universal-time timestamp) + (declare (ignore day-of-week dst-p)) + ;; Convert Lisp timezone (hours west) to standard ISO offset (hours/mins east/west) + (multiple-value-bind (tz-hours tz-mins) (truncate (* tz 60)) + (let ((sign (if (<= tz-hours 0) "+" "-")) + (abs-hours (abs (truncate tz-hours 60))) + (abs-mins (abs tz-mins))) + (format nil "~4,'0D-~2,'0D-~2,'0D ~2,'0D:~2,'0D:~2,'0D ~A~2,'0D~2,'0D" + year month date hour minute second + sign abs-hours abs-mins)))))) + +(defun pvs2alist-proof (proof &optional default-proof) `(("id" . ,(string (pvs:id proof))) ("description" . ,(pvs:description proof)) ("script" . ,(pvs:script proof)) - ("status" . ,(pvs:status proof)))) + ("status" . ,(pvs:status proof)) + ("is-default" . ,(if (eq default-proof proof) "yes" "no")) + ("create-date" . ,(print-timestamp-as-iso (pvs::create-date proof))) + ("run-date" . ,(print-timestamp-as-iso (pvs::run-date proof))))) (defrequest all-proofs-of-formula (form-ref) "Returns all the proofs associated with the given formula." (let* ((fdecl (pvs:get-formula-decl form-ref)) (proofs (pvs:proofs fdecl))) - (mapcar #'pvs2alist-proof proofs))) + (mapcar (lambda (p) (pvs2alist-proof p (pvs:default-proof fdecl))) proofs))) (defrequest delete-proof-of-formula (form-ref proof-id) "Deletes the proof-id of the formula." @@ -674,3 +696,18 @@ Returns JSON of the form: `(("main-file" . ,(format nil "~a" main-tex-file)))))) ;; END LaTeX Generation --------------------------------------------------- + +;; BEGIN Pretty-print Expanded -------------------------------------------- + +(defrequest prettyprint-expanded (theory-ref) + "Returns the pretty-print expanded form of the given theory" + (let ((theory (pvs::get-typechecked-theory theory-ref)) + (pvs::*no-comments* nil) + (pvs::*unparse-expanded* t) + (pvs::*xt-periods-allowed* t)) + (let ((thstring (pvs::unparse theory + :string t + :char-width sb-runtime::*default-char-width*))) + thstring))) + +;; END Pretty-print Expanded ---------------------------------------------- diff --git a/src/macros.lisp b/src/macros.lisp index ab6a42ef6..ae349bc4e 100644 --- a/src/macros.lisp +++ b/src/macros.lisp @@ -1,11 +1,6 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -*- Mode: Lisp -*- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; macros.lisp -- ;; Author : Sam Owre -;; Created On : Sun Jan 9 18:44:56 1994 -;; Last Modified By: Sam Owre -;; Last Modified On: Fri Dec 14 13:20:02 2012 -;; Update Count : 16 -;; Status : Stable ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -------------------------------------------------------------------- @@ -41,19 +36,44 @@ ;;; Note that there may be other ways to generate base-strings, but these are ;;; the two most common uses in PVS. +;; #+sbcl +;; (eval-when (:compile-toplevel :load-toplevel :execute) +;; (pushnew '(sb-ext:*print-vector-length* . nil) +;; sb-ext:*debug-print-variable-alist* +;; :test #'equal)) + +#+sbcl +(eval-when (:compile-toplevel :load-toplevel :execute) + (unless (fboundp '%orig-string) + (setf (symbol-function '%orig-string) (symbol-function 'string)))) + +#+sbcl +(sb-ext:without-package-locks + (defun string (obj) + "Redefinition of string to return (vector charater). +The original definition is in 'orig-string." + (coerce (funcall #'%orig-string obj) '(vector character)))) + #+sbcl (eval-when (:compile-toplevel :load-toplevel :execute) - (unless (fboundp 'orig-format) - (setf (symbol-function 'orig-format) (symbol-function 'format)))) + (unless (fboundp '%orig-format) + (setf (symbol-function '%orig-format) (symbol-function 'format)))) #+sbcl (sb-ext:without-package-locks (defun format (destination control-string &rest format-arguments) "Redefinition of format to return (vector charater) when a string is returned. The original definition is in 'orig-format." - (let ((result (apply #'orig-format destination control-string format-arguments))) + (let ((result (apply #'%orig-format destination control-string format-arguments))) (if (typep result 'base-string) (coerce result '(vector character)) result)))) +;; The above doesn't work in when compiled for optimization - seems to bring +;; in the original format +(defun sformat (control-string &rest format-arguments) + "Replaces format nil, as otherwise it returns a simple-base-string, +which prints as, e.g., #A((1) BASE-CHAR . \"1\") instead of \"1\"" + (coerce (apply #'format nil control-string format-arguments) '(vector character))) + (defmacro tcdebug (ctl &rest args) `(when *tcdebug* (if *to-emacs* diff --git a/src/makes.lisp b/src/makes.lisp index f2ede6cef..71f953298 100644 --- a/src/makes.lisp +++ b/src/makes.lisp @@ -1077,13 +1077,14 @@ (assert (symbolp id)) (assert (or (null description) (stringp description))) (assert (typep script '(or list justification))) + (let ((nscript (if (= (length script) 3) + (append script (list nil)) + script))) (make-instance 'tcc-proof-info :id id :description description :create-date create-date - :script (if (= (length script) 3) - (append script (list nil)) - script) + :script (sexp-unparse nscript) ;; make sure labels are all (vector character) :refers-to (typecase (car refers-to) (declaration refers-to) (declaration-entry @@ -1091,20 +1092,21 @@ (t (mapcar #'get-referenced-declaration (remove-if #'null refers-to)))) :origin (make-tcc-origin origin) - :decision-procedure-used decision-procedure)) + :decision-procedure-used decision-procedure))) (defun make-proof-info (script &optional id description) (assert (symbolp id)) (assert (or (null description) (stringp description))) (assert (typep script '(or list justification))) ;;(assert (not (null script))) - (make-instance 'proof-info - :id id - :description description - :script (if (= (length script) 3) - (append script (list nil)) - script) - :create-date (get-universal-time))) + (let ((nscript (if (= (length script) 3) + (append script (list nil)) + script))) + (make-instance 'proof-info + :id id + :description description + :script (sexp-unparse nscript) ;; make sure labels are all (vector character) + :create-date (get-universal-time)))) (defun make-tcc-proof-info (script &optional id description origin) (assert (symbolp id)) diff --git a/src/pp.lisp b/src/pp.lisp index ca46b6a57..948ec4dcc 100644 --- a/src/pp.lisp +++ b/src/pp.lisp @@ -2394,16 +2394,16 @@ then uses unpindent* to add the indent to each line" (write op) (write " "))))))) -(defgeneric collect-infix-conjuncts (ex &optional conjs)) +(defgeneric collect-infix-conjuncts (ex)) -(defmethod collect-infix-conjuncts ((ex infix-conjunction) &optional conjs) +(defmethod collect-infix-conjuncts ((ex infix-conjunction)) (if (= (parens ex) 0) - (collect-infix-conjuncts (args2 ex) - (collect-infix-conjuncts (args1 ex) conjs)) - (reverse (cons ex conjs)))) + (nconc (collect-infix-conjuncts (args1 ex)) + (collect-infix-conjuncts (args2 ex))) + (list ex))) -(defmethod collect-infix-conjuncts (ex &optional conjs) - (reverse (cons ex conjs))) +(defmethod collect-infix-conjuncts (ex) + (list ex)) (defmethod collect-infix-disjuncts ((ex infix-disjunction)) (if (= (parens ex) 0) diff --git a/src/prover/eproofcheck.lisp b/src/prover/eproofcheck.lisp index 0f852162d..afe06c5a6 100644 --- a/src/prover/eproofcheck.lisp +++ b/src/prover/eproofcheck.lisp @@ -292,7 +292,7 @@ (*top-proofstate* (make-instance 'top-proofstate :current-goal sequent - :label (string (id decl)) + :label (coerce (string (id decl)) '(vector character)) :strategy (if strategy strategy (query*-step)) @@ -496,94 +496,93 @@ (not (listp (car step))))) (cdr scr-new))))) -;; Modified by MM to inclue auto-fix [February 19, 2020] +;; Modified by M3 to inclue auto-fix [February 19, 2020] (defun save-proof-info (decl init-real-time init-run-time) - (unless (and (current-session)) - (let* ((prinfo (let ((sess (current-session))) - (if sess - (make-prf-info decl nil (id sess) "") - (default-proof decl)))) - (script (extract-justification-sexp - (collect-justification *top-proofstate*))) - (auto-fixed-prf - ;; if the prf was rerun in *auto-fix-on-rerun* mode and it ended proved, save it. - (and *auto-fix-on-rerun* - (eq (status-flag *top-proofstate*) '!) - (not *context-modified*)))) - (cond ((or (null (script prinfo)) - (equal (script prinfo) '("" (postpone) nil nil)) - (and (tcc-decl? decl) - (equal (script prinfo) (tcc-strategy decl)) - (not (or (equal script (tcc-strategy decl)) - (equal script (append (tcc-strategy decl) '(nil nil)))))) - (and (eq (status prinfo) 'proved) - (eq (status-flag *top-proofstate*) '!) - (or - ;; next check is added to avoid crashing on malformed prf files. - ;; should be handled another way (TODO) - (not (or (equalp (car (script prinfo)) "") - (and (stringp (car (script prinfo))) - (char= (char (car (script prinfo)) 0) #\;)))) - (script-structure-changed? prinfo script)))) - (setf (script prinfo) script)) - ((and (or (not *proving-tcc*) auto-fixed-prf) - (or (not *noninteractive*) auto-fixed-prf) - script - (not (equal script '("" (postpone) nil nil))) - (not (equal (script prinfo) script)) - (or (pvs-noquestions *proof-prompt-behavior*) - auto-fixed-prf - (let ((ids (mapcar #'id - (remove-if-not - #'(lambda (prinfo) - (equal (script prinfo) script)) - (proofs decl))))) - (pvs-yes-or-no-p - "~@[This proof is already associated with this formula ~ + (let* ((prinfo (let ((sess (current-session))) + (if sess + (make-prf-info decl nil (id sess) "") + (default-proof decl)))) + (script (extract-justification-sexp + (collect-justification *top-proofstate*))) + (auto-fixed-prf + ;; if the prf was rerun in *auto-fix-on-rerun* mode and it ended proved, save it. + (and *auto-fix-on-rerun* + (eq (status-flag *top-proofstate*) '!) + (not *context-modified*)))) + (cond ((or (null (script prinfo)) + (equal (script prinfo) '("" (postpone) nil nil)) + (and (tcc-decl? decl) + (equal (script prinfo) (tcc-strategy decl)) + (not (or (equal script (tcc-strategy decl)) + (equal script (append (tcc-strategy decl) '(nil nil)))))) + (and (eq (status prinfo) 'proved) + (eq (status-flag *top-proofstate*) '!) + (or + ;; next check is added to avoid crashing on malformed prf files. + ;; should be handled another way (TODO) + (not (or (equalp (car (script prinfo)) "") + (and (stringp (car (script prinfo))) + (char= (char (car (script prinfo)) 0) #\;)))) + (script-structure-changed? prinfo script)))) + (setf (script prinfo) script)) + ((and (or (not *proving-tcc*) auto-fixed-prf) + (or (not *noninteractive*) auto-fixed-prf) + script + (not (equal script '("" (postpone) nil nil))) + (not (equal (script prinfo) script)) + (or (pvs-noquestions *proof-prompt-behavior*) + auto-fixed-prf + (let ((ids (mapcar #'id + (remove-if-not + #'(lambda (prinfo) + (equal (script prinfo) script)) + (proofs decl))))) + (pvs-yes-or-no-p + "~@[This proof is already associated with this formula ~ as ~{~a~^, ~}~%~]~ Would you like the proof to be saved~@[ anyway~]? " - ids ids)))) - (cond ((and (not auto-fixed-prf) - (or (pvs-noquestions *proof-prompt-behavior*) - (pvs-yes-or-no-p - "Would you like to overwrite the current proof (named ~a)? " - (id prinfo)))) - (when (pvs-dont-ask *proof-prompt-behavior*) - (format t "Overwriting proof named ~a" (id prinfo))) - (setf (script prinfo) script)) - ((let ((sess (current-session))) - (when sess - ;; Note that it isn't made the default - (setf (script prinfo) script)))) - (t (let ((id (read-proof-id (next-proof-id decl))) - (description (read-proof-description))) - (setq prinfo - (make-default-proof decl script id - description))))))) - (setf (real-time prinfo) (realtime-since init-real-time)) - (setf (run-time prinfo) (runtime-since init-run-time)) - (setf (run-date prinfo) (get-universal-time)) - (when *use-default-dp?* - (setf (decision-procedure-used prinfo) *default-decision-procedure*)) - (setf (proof-status decl) - (if (eq (status-flag *top-proofstate*) '!) - (cond (*context-modified* - (pvs-message "~a proved with modified context, so marked unchecked" - (id decl)) - 'unchecked) - (t 'proved)) - 'unfinished)) - (format-nif "~%~%Run time = ~,2,-3F secs." (run-time prinfo)) - (format-nif "~%Real time = ~,2,-3F secs.~%" (real-time prinfo)) - (when (and *context-modified* - (eq (proof-status decl) 'proved)) - (setf (proof-status decl) 'unfinished) - (when (and (not *proving-tcc*) - (pvs-yes-or-no-p - "~%Context was modified in mid-proof. ~ + ids ids)))) + (cond ((and (not auto-fixed-prf) + (or (pvs-noquestions *proof-prompt-behavior*) + (pvs-yes-or-no-p + "Would you like to overwrite the current proof (named ~a)? " + (id prinfo)))) + (when (pvs-dont-ask *proof-prompt-behavior*) + (format t "Overwriting proof named ~a" (id prinfo))) + (setf (script prinfo) script)) + ((let ((sess (current-session))) + (when sess + ;; Note that it isn't made the default + (setf (script prinfo) script)))) + (t (let ((id (read-proof-id (next-proof-id decl))) + (description (read-proof-description))) + (setq prinfo + (make-default-proof decl script id + description))))))) + (setf (real-time prinfo) (realtime-since init-real-time)) + (setf (run-time prinfo) (runtime-since init-run-time)) + (setf (run-date prinfo) (get-universal-time)) + (when *use-default-dp?* + (setf (decision-procedure-used prinfo) *default-decision-procedure*)) + (setf (proof-status decl) + (if (eq (status-flag *top-proofstate*) '!) + (cond (*context-modified* + (pvs-message "~a proved with modified context, so marked unchecked" + (id decl)) + 'unchecked) + (t 'proved)) + 'unfinished)) + (format-nif "~%~%Run time = ~,2,-3F secs." (run-time prinfo)) + (format-nif "~%Real time = ~,2,-3F secs.~%" (real-time prinfo)) + (when (and *context-modified* + (eq (proof-status decl) 'proved)) + (setf (proof-status decl) 'unfinished) + (when (and (not *proving-tcc*) + (pvs-yes-or-no-p + "~%Context was modified in mid-proof. ~ Would you like to rerun the proof?~%")) - (let ((*in-checker* nil)) - (prove-decl decl :strategy '(then (rerun) (query*))))))))) + (let ((*in-checker* nil)) + (prove-decl decl :strategy '(then (rerun) (query*)))))))) ;; Modified by MM to inclue auto-fix [February 19, 2020] (defun read-proof-id (default) @@ -838,10 +837,10 @@ (setf (status-flag proofstate) '! (current-rule proofstate) '(propax) (printout proofstate) - (format nil "~%which is trivially true.") + (sformat "~%which is trivially true.") (justification proofstate) (make-instance 'justification - :label (label-suffix (label proofstate)) + :label (coerce (label-suffix (label proofstate)) '(vector character)) :rule '(propax))) proofstate) ;;else display goal, ;;eval strategy, invoke rule-apply @@ -898,7 +897,7 @@ (integerp *rerunning-proof-message-time*) (> (realtime-since *rerunning-proof-message-time*) 3000)) ;;print mini-buffer msg - (setq *rerunning-proof* (format nil "~a." *rerunning-proof*)) + (setq *rerunning-proof* (sformat "~a." *rerunning-proof*)) (setq *rerunning-proof-message-time* (get-internal-real-time)) (pvs-message *rerunning-proof*)) @@ -978,7 +977,7 @@ (defun write-prover-log () (when nil ;;*prover-log* - (let* ((logfile (format nil "~a/prooflog-~a.json" + (let* ((logfile (sformat "~a/prooflog-~a.json" *pvs-log-directory* (subseq (iso8601-date) 0 10))) (prlog (jsonify-prover-log))) (with-open-file (out logfile :direction :output @@ -1035,7 +1034,7 @@ (when (and pp (or quiet-flag (not *suppress-printing*))) (let ((pp (if (consp pp) - (apply #'format nil + (apply #'sformat (car pp) (mapcar #'(lambda (x) (if (stringp x) @@ -1551,7 +1550,7 @@ (if (char= (char suffix lcpos) #\T) (setq suffix (subseq suffix 0 lcpos))) (if (every #'digit-char-p suffix) - suffix + (coerce suffix '(vector character)) "")) ""))) @@ -2523,7 +2522,7 @@ :label (if (= (length allsubgoals) 1) (label proofstate) - (format nil "~a.~a~@[T~]" (label proofstate) + (sformat "~a.~a~@[T~]" (label proofstate) goalnum (memq goal tcc-subgoals))) :subgoalnum (1- goalnum) :proof-dependent-decls proof-dependent-decls @@ -2614,10 +2613,10 @@ x)) (defmethod pc-parse (input nt) - (parse :string (format nil "~a" input) :nt nt)) + (parse :string (sformat "~a" input) :nt nt)) (defmethod pc-parse ((input integer) nt) - (parse :string (format nil "~a" input) :nt nt)) + (parse :string (sformat "~a" input) :nt nt)) (defmethod pc-parse ((input syntax) nt) (declare (ignore nt)) @@ -2747,7 +2746,9 @@ (defun sexp-unparse (form) (cond ((consp form)(cons (sexp-unparse (car form)) (sexp-unparse (cdr form)))) - ((or (null form)(symbolp form)(numberp form) (stringp form)) + ((stringp form) + (coerce form '(vector character))) ;; + ((or (null form) (symbolp form) (numberp form)) form) ((typep form 'justification) (copy form 'label (sexp-unparse (label form)) @@ -2766,7 +2767,7 @@ (declared-type form)) (type form))) :string t))) - (t (format nil "~a" form)))) + (t (sformat "~a" form)))) (defmethod extract-justification-sexp ((list list)) (cond ((null list) nil) @@ -2782,7 +2783,7 @@ ;;; ++ here means two or more. (defun editable-justification (justif &optional - label xflag full-label no-escape?) + label xflag full-label (no-escape? t)) ;;NSH(1.3.98) if full-label is given, then the full label is ;;printed rather than just the branch numbers. (unless (null justif) @@ -2798,7 +2799,7 @@ (full-label (if (and full-label (not (equal jlabel label)) (> (length jlabel) 0)) - (format nil "~a.~a" full-label jlabel) + (sformat "~a.~a" full-label jlabel) full-label)) (ejustif (cons top-step (editable-justification* (subgoals justif) @@ -3523,7 +3524,7 @@ (when skoconsts (format stream "~%Skolem-constants:") (dolist (sc skoconsts) - (let* ((decl (format nil "~a: ~a" (id sc) (type sc))) + (let* ((decl (sformat "~a: ~a" (id sc) (type sc))) (def (when (definition sc) (unpindent (definition sc) 5 :string t)))) (format stream "~% ~a~@[ = ~a~]" decl def)))))) @@ -3952,10 +3953,10 @@ (if newline-position (let ((preline (subseq comment-string 0 newline-position)) (postline (subseq comment-string (1+ newline-position)))) - (format nil ";;; ~a~%~a" + (sformat ";;; ~a~%~a" preline (semi-colonize postline))) - (format nil ";;; ~a" comment-string)))) + (sformat ";;; ~a" comment-string)))) (defun comment-step (string) #'(lambda (ps) @@ -4059,5 +4060,5 @@ (defun unique-ps-id (ps &optional (label (label ps)) (num 0)) (let ((par-ps (parent-proofstate ps))) (if (or (null par-ps) (not (string= (label par-ps) label))) - (format nil "~a-~d" label num) + (sformat "~a-~d" label num) (unique-ps-id par-ps label (1+ num))))) diff --git a/src/pvs-threads.lisp b/src/pvs-threads.lisp index afc177ce2..32b4482cc 100644 --- a/src/pvs-threads.lisp +++ b/src/pvs-threads.lisp @@ -219,7 +219,7 @@ Sends a quit, waits half a sec, then kills the thread, and moves the session to (dolist (sess *all-sessions*) (if (session-alive-p sess) (let ((id (id sess))) - (handler-case (bt:with-timeout (3) (prover-step id "(quit)")) + (handler-case (bt:with-timeout (3) (prover-step (symbol-name id) "(quit)")) (bt:timeout () (session-kill sess)))) (session-kill sess)))) diff --git a/src/pvs.lisp b/src/pvs.lisp index 2481d3c20..e0c4671ce 100644 --- a/src/pvs.lisp +++ b/src/pvs.lisp @@ -44,14 +44,6 @@ (defvar *parsed-theories-seen* nil) -(defstruct pvs-meta-info - version - environment - patch-files - strategy-files - lisp-files - libfiles) - ;; M3: This debugger is used when running the rpc server to automatically abort ;; to top-level on any signal, so they don't affect the server responsiveness [Sept 2020]. ;; (defun rpc-mode-debugger (condition me-or-my-encapsulation) @@ -815,12 +807,13 @@ use binfiles." new-theories)) (setq *context-modified* t)) (dolist (sess *all-sessions*) - (let ((sess-th (module (formula-decl sess)))) - (when (some #'(lambda (cth) - (or (eq cth sess-th) - (memq cth (all-importings sess-th)))) - new-theories) - (prover-step (id sess) "(lisp (setq *context-modified* t))")))) + (when (proof-session? sess) + (let ((sess-th (module (formula-decl sess)))) + (when (some #'(lambda (cth) + (or (eq cth sess-th) + (memq cth (all-importings sess-th)))) + new-theories) + (prover-step (id sess) "(lisp (setq *context-modified* t))"))))) (values new-theories nil t))))))) (defun parse-all-pvs-files (dir) @@ -1391,11 +1384,10 @@ escapes here." (otail (memq odecl (all-decls othy))) (last-kept-decl (unless (or (formal-decl? odecl) (generated-by odecl)) - ;;NSH(5-27-26): moved remove-if out of ldiff - ;;otherwise the null-compare assert in merged-parsed-theory-decls fails (car (last (remove-if #'(lambda (d) (or (formal-decl? d) - (generated-by d))) + (and (generated-by d) + (tcc? d)))) (ldiff (all-decls othy) otail))))))) @@ -2827,6 +2819,7 @@ Note that even proved ones get overwritten" (terpri out) (terpri out))))) (theory-decl (format nil "~a.~a" (id theory) (decl-to-declname decl))) (buffer (format nil "~a.~a.tccs" (id theory) (decl-to-declname decl)))) + (declare (ignorable unparsed-a-tcc?)) (cond ((not (string= str "")) (let ((*valid-id-check* nil)) (setf (tcc-form decl) @@ -2836,7 +2829,7 @@ Note that even proved ones get overwritten" (pvs-buffer buffer str t t) theory-decl) (t (pvs-message "Declaration ~a.~a has no TCCs" - (id theory) (decl-to-declname decl)))))) + (id theory) (decl-to-declname decl)))))) ;;; Given a declaration, returns a declname, used to create the ;;; show-declaration-tccs buffer. For a declaration with an id, this is diff --git a/src/subst-mod-params.lisp b/src/subst-mod-params.lisp index 72418b42f..fcb5c8c87 100644 --- a/src/subst-mod-params.lisp +++ b/src/subst-mod-params.lisp @@ -1250,7 +1250,7 @@ (dolist (decl (all-decls nth)) (when (declaration? decl) (setf (module decl) nth) - (setf (refers-to decl) (regenerate-xref decl)))) + (regenerate-xref decl))) (setf (all-usings nth) (let ((imps nil)) (maphash #'(lambda (th thinsts) @@ -1329,7 +1329,7 @@ (id decl)))) (setf (generated ndecl) (remove-if #'tcc? (generated ndecl))) ;; (when (generated ndecl) (break "subst-mod-params-decls with generated")) - (when bval + (when (and bval (not (var-decl? ndecl))) (if (actual? bval) (cond ((type-value bval) (let* ((tval (type-value bval)) @@ -2655,8 +2655,10 @@ lift[T: TYPE]: DATATYPE BEGIN | lift_nat: DATATYPE BEGIN (cond ((declaration? bdg) (let* ((ndacts (when dacts (subst-mod-params* dacts modinst bindings))) (mi (if (eq (id (module-instance expr)) (id modinst)) - (lcopy modinst :dactuals ndacts) - (progn (when (formals (module bdg)) + (lcopy modinst :dactuals ndacts + :actuals (unless (var-decl? bdg) (actuals modinst))) + (progn (when (and (formals (module bdg)) + (not (var-decl? decl))) (break "name-expr no actuals available")) (make-theoryname (module bdg))))) ;;(alist (mapcar #'cons (decl-formals decl) (decl-formals bdg))) @@ -2670,20 +2672,17 @@ lift[T: TYPE]: DATATYPE BEGIN | lift_nat: DATATYPE BEGIN ((actual? bdg) (if dacts (let* ((ex (expr bdg)) - (nex (subst-acts-in-form ex bindings)) + (nex1 (subst-acts-in-form ex bindings)) (adecl (when dacts (if (name-expr? ex) (declaration ex) (break "dacts1a")))) (dfmls (when dacts (decl-formals adecl))) (sdacts (when dacts (subst-mod-params* dacts modinst bindings))) - (nex (if dacts - (subst-for-formals - nex - (mapcar #'(lambda (x y) (cons x (type-value y))) - dfmls sdacts)) - nex)) - ) + (nex (subst-for-formals + nex1 + (mapcar #'(lambda (x y) (cons x (type-value y))) + dfmls sdacts)))) #+badassert (assert (every #'(lambda (fp) (or (memq fp (decl-formals (current-declaration))) @@ -3142,6 +3141,14 @@ lift[T: TYPE]: DATATYPE BEGIN | lift_nat: DATATYPE BEGIN (cdr obindings) modinst bindings (cons nbinding nbindings))) (nreverse nbindings))) +(defmethod subst-mod-params* ((expr array-expr) modinst bindings) + (let ((nexpr (call-next-method)) + (nexprs (subst-mod-params* (exprs expr) modinst bindings))) + (cond ((eq nexpr expr) + (lcopy nexpr :exprs nexprs)) + (t (setf (exprs nexpr) nexprs) + nexpr)))) + (defmethod subst-mod-params* ((expr update-expr) modinst bindings) (with-slots (expression assignments type) expr (let ((nexpr (subst-mod-params* expression modinst bindings)) diff --git a/src/substit.lisp b/src/substit.lisp index a3beb78d9..916a42473 100644 --- a/src/substit.lisp +++ b/src/substit.lisp @@ -1,11 +1,6 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -*- Mode: Lisp -*- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; substit.lisp -- ;; Author : N. Shankar -;; Created On : Thu Oct 27 00:15:26 1994 -;; Last Modified By: Sam Owre -;; Last Modified On: Fri Oct 30 16:54:32 1998 -;; Update Count : 6 -;; Status : Stable ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -------------------------------------------------------------------- @@ -206,16 +201,24 @@ it is nil in the substituted binding") ((typep (cdr binding) 'binding) (if (eq (car binding) (cdr binding)) expr - (let ((nex (if (typep (cdr binding) 'field-decl) - (change-class (copy (cdr binding)) - 'field-name-expr) - (change-class (copy (cdr binding)) - 'name-expr)))) + (let* ((nex (if (typep (cdr binding) 'field-decl) + (change-class (copy (cdr binding)) + 'field-name-expr) + (change-class (copy (cdr binding)) + 'name-expr))) + (eres (resolution expr)) + (nres (if (conversion-resolution? eres) + (make-instance 'conversion-resolution + :module-instance (substit* (module-instance expr) alist) + :declaration (cdr binding) + :type (substit* (type eres) alist) + :conversion (conversion eres)) + (mk-resolution (cdr binding) + (current-theory-name) + (type (cdr binding)))))) (setf (parens nex) 0) - (setf (resolutions nex) - (list (mk-resolution (cdr binding) - (current-theory-name) - (type (cdr binding))))) + (setf (resolutions nex) (list nres)) + (setf (type nex) (type nres)) #+pvsdebug (assert (or (eq nex expr) (not (tc-eq nex expr)))) nex))) @@ -379,34 +382,39 @@ it is nil in the substituted binding") (make!-injection?-application (index op) arg (actuals op))) (extraction-expr (make!-extraction-application (index op) arg (actuals op))))) - (t (let* ((stype (find-supertype (type op))) - (nex (simplify-or-copy-app - expr op arg - (if (typep (domain stype) 'dep-binding) - (new-substit-hash - (substit* (range stype) - (acons (domain stype) - arg nil))) - (range stype))))) - (cond ((not (application? nex)) - (if (compatible? (type expr) (type nex)) - nex - (let ((sexpr (subst-mod-params nex - (theory-instance (current-declaration))))) - sexpr))) - ((and (not (compatible? (dep-binding-type (domain stype)) - (type (argument nex)))) - (assuming-tcc? (current-declaration)) - (theory-instance (current-declaration)) - (mappings (theory-instance (current-declaration)))) - (let ((sexpr (subst-mod-params nex - (theory-instance (current-declaration))))) - sexpr)) - (t ;; Note: the copy :around (application) method takes care of - ;; changing the class if it is needed. - (if (strong-tc-eq nex expr) - expr - nex))))))))) + (t (let ((stype (find-supertype (type op)))) + (if (funtype? stype) + (let ((nex (simplify-or-copy-app + expr op arg + (if (typep (domain stype) 'dep-binding) + (new-substit-hash + (substit* (range stype) + (acons (domain stype) + arg nil))) + (range stype))))) + (cond ((not (application? nex)) + (if (compatible? (type expr) (type nex)) + nex + (let ((sexpr (subst-mod-params nex + (theory-instance (current-declaration))))) + sexpr))) + ((and (not (compatible? (dep-binding-type (domain stype)) + (type (argument nex)))) + (assuming-tcc? (current-declaration)) + (theory-instance (current-declaration)) + (mappings (theory-instance (current-declaration)))) + (let ((sexpr (subst-mod-params nex + (theory-instance (current-declaration))))) + sexpr)) + (t ;; Note: the copy :around (application) method takes care of + ;; changing the class if it is needed. + (if (strong-tc-eq nex expr) + expr + nex)))) + (let ((*no-conversions-allowed* nil) + (app (mk-application op arg))) + ;;(set-type* app (substit* (type expr) alist)) + (tc-expr (str app) :expected (substit* (type expr) alist)))))))))) (defmethod substit* :around ((expr let-expr) alist) (declare (ignore alist)) diff --git a/src/utils.lisp b/src/utils.lisp index 3c37bdaa4..c4c9deedf 100644 --- a/src/utils.lisp +++ b/src/utils.lisp @@ -5421,20 +5421,44 @@ we can get this method using ;; } (defun pvs-meta-info () - (lcons :pvs-version *pvs-version* - :pvs-path *pvs-path* - :lisp-version (lisp-implementation-version) - :emacs-version (pvs-emacs-eval "(emacs-version)") - :pvs-executable (get-file-ref (car (uiop:raw-command-line-arguments))) - :lisp-patches (get-patches-info) - :strategies-files (mapcar #'get-file-ref - (cdr (assq :strategies *files-loaded*))) - :pvs-environment-variables (mapcan #'(lambda (var) - (let ((val (environment-variable - (string var)))) - (when val - (list (cons var val))))) - *pvs-environment-variables*))) + (lcons "pvs-version" *pvs-version* + "pvs-path" *pvs-path* + "lisp-version" (lisp-implementation-version) + "emacs-version" (pvs-emacs-eval "(emacs-version)") + "pvs-executable" (get-file-ref (car (uiop:raw-command-line-arguments))) + "lisp-patches" (get-patches-info) + "strategies-files" (mapcar #'get-file-ref + (cdr (assq :strategies *files-loaded*))) + "pvs-environment-variables" (mapcan #'(lambda (var) + (let ((val (environment-variable + (string var)))) + (when val + (list (cons var val))))) + *pvs-environment-variables*) + "version-control" (when (and (git-available-p) (in-git-repo-p *pvs-path*)) + (multiple-value-bind (short-commit long-commit) (git-current-commit) + (let ((git-description (pvs-git-description)) + (branch-description (git-current-branch)) + (commit-date (git-current-commit-date))) + `(("short-hash" . ,short-commit) + ("long-hash" . ,long-commit) + ("description" . ,(pvs-git-description)) + ("branch-info" . ,(git-current-branch)) + ("commit-date" . ,(git-current-commit-date)))))) + "build-date" (when *pvs-build-time* + (handler-case + (multiple-value-bind (second minute hour date month year day-of-week dst-p tz) + (decode-universal-time *pvs-build-time*) + (declare (ignore day-of-week dst-p)) + ;; Convert Lisp timezone (hours west) to standard ISO offset (hours/mins east/west) + (multiple-value-bind (tz-hours tz-mins) (truncate (* tz 60)) + (let ((sign (if (<= tz-hours 0) "+" "-")) + (abs-hours (abs (truncate tz-hours 60))) + (abs-mins (abs tz-mins))) + (format nil "~4,'0D-~2,'0D-~2,'0D ~2,'0D:~2,'0D:~2,'0D ~A~2,'0D~2,'0D" + year month date hour minute second + sign abs-hours abs-mins)))) + (error () nil))))) (defun get-lisp-exec-info () (list (get-file-ref (format nil "~a/pvs" *pvs-path*)) @@ -5810,6 +5834,13 @@ and the next method is called with this. Only \formula\" is required." #\:)) (error "*pvs-path* has no .git directory"))) +(defun git-current-commit-date () + (when (in-git-repo-p *pvs-path*) + (uiop:run-program (format nil "git -C ~a log -1 --format=%cd --date=iso" *pvs-path*) + :input "//dev//null" + :output '(:string :stripped t)))) + + (defun in-git-repo-p (path) "Check if the given PATH is inside a Git repository." (let ((result (ignore-errors @@ -6137,10 +6168,12 @@ Walks through each script, collecting ngrams for each strategy name. 1-grams are (t (flatten-proof-script-list (break "flatten-proof-script-list")))))) #+sbcl -(defun dbg () +(defun dbg (&optional (on t)) "Sets optimization for debugging, giving more visibility to subsequently loaded files and defuns." - (proclaim '(optimize (safety 3) (speed 0) (cl:debug 3)))) + (if on + (proclaim '(optimize (speed 0) (safety 3) (cl:debug 3))) + (proclaim '(optimize (speed 3) (safety 1) (cl:debug 0))))) #+sbcl (defun control-stack-size ()