search

snu-sf / CompCertM

6 stars 5 forks source link

[DO NOT MERGE] v3.11 #25

Open kim-yoonseung opened 1 year ago

kim-yoonseung commented 1 year ago

CompCertM 을 다음 일에 사용하려는데, Coq 버전을 올리고 싶어서 CompCert 버전을 3.11로 올렸습니다. Makefile에 -R ../XX compcertr.XX 를 추가해줘야 컴파일이 되던데, 무슨 차이인지 모르겠네요.

저는 일단 이 위에서 작업을 할 계획입니다. 지금 v3.9 브랜치에다가 pull request를 만들었는데요, 혹시 머지하실 생각 있으시면 따로 브랜치를 만들고 고치고 싶은 부분 고치고 푸시하셔도 될 것 같습니다.

kim-yoonseung commented 1 year ago

CompCert 3.12가 최신 버전이긴 한데, Selectionproof.v에서 eventually 라는 정의를 사용하게 되면서 증명이 어려워져서 3.11까지만 올렸습니다.