Bug 593

Summary: please revert removal of proof* from .gitignore
Product: Libre-SOC's first SoC Reporter: Luke Kenneth Casson Leighton <lkcl>
Component: Source CodeAssignee: Cole Poirier <colepoirier>
Status: RESOLVED FIXED    
Severity: enhancement CC: cestrauss, libre-soc-bugs
Priority: ---    
Version: unspecified   
Hardware: PC   
OS: Linux   
NLnet milestone: --- total budget (EUR) for completion of task and all subtasks: 0
budget (EUR) for this task, excluding subtasks' budget: 0 parent task for budget allocation:
child tasks for budget allocation: The table of payments (in EUR) for this task; TOML format:

Description Luke Kenneth Casson Leighton 2021-02-09 19:48:18 GMT
commit eec81fdbe13f0caa0c3ccf3b4134ccaebc6c87be
Author: colepoirier <colepoirier@gmail.com>
Date:   Sun Feb 7 14:30:16 2021 -0800

    Modify experiment/formal/.gitignore because was preventing commiting
    proof_icache.py

please revert this and fix the name of the file.  you've interfered
with people running "git status".
Comment 1 Cole Poirier 2021-02-09 21:33:02 GMT
(In reply to Luke Kenneth Casson Leighton from comment #0)
> commit eec81fdbe13f0caa0c3ccf3b4134ccaebc6c87be
> Author: colepoirier <colepoirier@gmail.com>
> Date:   Sun Feb 7 14:30:16 2021 -0800
> 
>     Modify experiment/formal/.gitignore because was preventing commiting
>     proof_icache.py
> 
> please revert this and fix the name of the file.  you've interfered
> with people running "git status".

What is the reason that formal proof file names cannot begin with proof?
Comment 2 Cesar Strauss 2021-02-09 21:52:56 GMT
When running proofs, it stores results under a directory named after the file, "proof_*/"

You can use "proof*/**" in the .gitignore, instead, to cover this.
Comment 3 Cole Poirier 2021-02-09 22:40:15 GMT
(In reply to Cesar Strauss from comment #2)
> When running proofs, it stores results under a directory named after the
> file, "proof_*/"
> 
> You can use "proof*/**" in the .gitignore, instead, to cover this.

Thanks Cesar, done.