Open
Conversation
Author
|
CompCert 3.12가 최신 버전이긴 한데, Selectionproof.v에서 eventually 라는 정의를 사용하게 되면서 증명이 어려워져서 3.11까지만 올렸습니다. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
CompCertM 을 다음 일에 사용하려는데, Coq 버전을 올리고 싶어서 CompCert 버전을 3.11로 올렸습니다.
Makefile에 -R ../XX compcertr.XX 를 추가해줘야 컴파일이 되던데, 무슨 차이인지 모르겠네요.
저는 일단 이 위에서 작업을 할 계획입니다.
지금 v3.9 브랜치에다가 pull request를 만들었는데요, 혹시 머지하실 생각 있으시면 따로 브랜치를 만들고 고치고 싶은 부분 고치고 푸시하셔도 될 것 같습니다.