We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
Cd
In coq/coq#11966 (comment), minimization fails because https://github.com/MetaCoq/metacoq/blob/ec967346ba76d1c888faabefe268a9cd0a2e6e09/template-coq/theories/Extraction.v#L112 works when gen-src already exists but fails when it does not. Perhaps we should detect Error: Cd failed: <DIRNAME>: No such file or directory and, when it is not the error we're looking for, recreate it, and keep a list of what directories we need to create in the same directory as each file? Or we can do a search for Cd in the source and generate this list ahead of time?
gen-src
Error: Cd failed: <DIRNAME>: No such file or directory
The text was updated successfully, but these errors were encountered:
No branches or pull requests
In coq/coq#11966 (comment), minimization fails because https://github.com/MetaCoq/metacoq/blob/ec967346ba76d1c888faabefe268a9cd0a2e6e09/template-coq/theories/Extraction.v#L112 works when
gen-src
already exists but fails when it does not. Perhaps we should detectError: Cd failed: <DIRNAME>: No such file or directory
and, when it is not the error we're looking for, recreate it, and keep a list of what directories we need to create in the same directory as each file? Or we can do a search forCd
in the source and generate this list ahead of time?The text was updated successfully, but these errors were encountered: