Skip to content

Feature/eng 452 remove functions to trackcsv#15

Open
silverboyir wants to merge 13 commits intomasterfrom
feature/ENG-452-remove-functions-to-trackcsv
Open

Feature/eng 452 remove functions to trackcsv#15
silverboyir wants to merge 13 commits intomasterfrom
feature/ENG-452-remove-functions-to-trackcsv

Conversation

@silverboyir
Copy link
Copy Markdown
Collaborator

No description provided.

avrevic and others added 7 commits February 19, 2026 17:22
…ocker flow

- Replaced  usage in  command with .
- Updated  command to respect  configuration (fixing script not found errors).
- Enhanced  in  to support preserving existing configuration fields.
- Updated  to support local Docker images by checking existence before pull.
- Fixed ARM64 compatibility by removing hardcoded  in runtime.
- Added Python dependencies to Dockerfile.
- Added CACHEBUST arg to Dockerfile and CI workflow to ensure fresh builds.
- Updated README with instructions for building and using local Docker images.
Copilot AI review requested due to automatic review settings February 19, 2026 20:40
Copy link
Copy Markdown
Contributor

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR implements a significant architectural change to make the verilib-cli tool more resilient by making previously required dependencies optional. The create command no longer requires functions_to_track.csv or the Python analysis script to succeed, and other commands will auto-create missing configuration files rather than failing. This enables a graceful degradation pattern where commands can continue with reduced functionality when optional dependencies are absent.

Changes:

  • Made functions_to_track.csv optional in the create command; when absent, the script tracks all functions by default (if script runs)
  • Made analyze_verus_specs_proofs.py script optional; create command continues without structure files if script is absent or fails
  • Added auto-creation of default config.json when missing, allowing commands to proceed rather than failing

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated 8 comments.

Show a summary per file
File Description
src/commands/create.rs Refactored to make seed path optional, handle script absence gracefully via try_run_analyze_verus_specs_proofs, and support both project and bundled script locations
src/structure/config.rs Added DEFAULT_CONFIG_JSON constant and logic to auto-create config when missing in ConfigPaths::load
src/commands/atomize.rs Added has_md_files check to write empty stubs.json when no structure files exist, preventing stubify failures
tests/structure_commands_test.rs Updated test names and assertions to reflect new optional behavior, removed fallback seed checks
README.md Updated documentation to clarify that script and CSV file are now optional

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Comment thread src/commands/create.rs Outdated
Comment thread src/commands/create.rs Outdated
Comment thread src/structure/config.rs
Comment thread src/commands/atomize.rs
Comment thread src/commands/create.rs Outdated
Comment thread tests/structure_commands_test.rs
Comment thread tests/structure_commands_test.rs
Comment thread src/commands/create.rs Outdated
@astefano
Copy link
Copy Markdown
Collaborator

We no longer need analyze_verus_specs_proofs.py.
We shouldn't commit functions_to_track.csv (the one in this repo represents the functions in this repo!).

Also, i notice docker stuff in structure; structure is supposed to be about managing verification structure files, these are data-layer concerns. We shouldn't leak docker stuff inside structure. There's this issue documenting it: #17.

Copilot AI review requested due to automatic review settings February 20, 2026 13:21
Copy link
Copy Markdown
Contributor

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copilot was unable to review this pull request because the user who requested the review is ineligible. To be eligible to request a review, you need a paid Copilot license, or your organization must enable Copilot code review.

@silverboyir silverboyir force-pushed the master branch 5 times, most recently from 1f8ff36 to 7f94348 Compare February 24, 2026 21:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants