Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove dependency on git to use starter-kit #128

Open
jimgrundy opened this issue Jul 11, 2022 · 3 comments
Open

Remove dependency on git to use starter-kit #128

jimgrundy opened this issue Jul 11, 2022 · 3 comments
Assignees
Labels
bug Something isn't working

Comments

@jimgrundy
Copy link
Contributor

Right now, if you attempt to use the starter kit outside of a Git repo you will get the following result:

cbmc % cbmc-starter-kit-setup
Traceback (most recent call last):
  File "/usr/local/bin/cbmc-starter-kit-setup", line 8, in <module>
    sys.exit(main())
  File "/usr/local/Cellar/cbmc-starter-kit/2.4/libexec/lib/python3.8/site-packages/cbmc_starter_kit/setup.py", line 73, in main
    source_root = repository.repository_root()
  File "/usr/local/Cellar/cbmc-starter-kit/2.4/libexec/lib/python3.8/site-packages/cbmc_starter_kit/repository.py", line 52, in repository_root
    raise UserWarning(f"No git repository contains {cwd}") from None
UserWarning: No git repository contains .

But, the starter kit seems to be becoming the default easy way for all users to get started using CBMC, and in this application the git dependency seems like an unneeded speed bump. If you are just starting out with CBMC or looking to evaluate it then the starter-kit should get you started fast.

Also, there are people out there who want to use CBMC with other version control systems. It would be a pitty of those people couldn't use the starter kit.

@markrtuttle
Copy link
Contributor

We could add a command line option that would let the user specify the root instead of searching for the root.

@jimgrundy
Copy link
Contributor Author

Maybe go further and make that the default with an option to infer the root if you are in a git repo.

@markrtuttle
Copy link
Contributor

markrtuttle commented Aug 10, 2022

Let's add command line options --git-root and --src-root flags to specify them from command line. The sequence of defaults is --git-root if specified else search for git root else None. The sequence of defaults is --src-root if specified else git root else None.

@feliperodri feliperodri added the bug Something isn't working label Nov 3, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

3 participants