Coq의 정리의 고속 계산

Question

매우 간단한 경우에도 Coq이 계산을 마칠 때까지 기다려야합니다.

"비동기 및 병렬 교정 처리"에 대해 알고 있지만 내 코드에는 고유 한 악의가 있다고 가정하므로 교정본의 모범 사례/권장 사항에 대한 참조 또는 조언을 받고 싶습니다. 예컨대 : 정의 대신 정리 (theorem)를 사용하는

1. 시도,

2. 사용 컴파일러. parrallel 처리를 사용하십시오. 더 나은 하드웨어를 사용하십시오.

(@functionname VAR1 ... varn)

3. 세미콜론처럼, 모든 인수를 작성 자리 표시자를 사용하지 마십시오

4. (;) 대신 기간의

5. 를 사용하는 것이 훨씬 빠릅니다 (.) "set (f : = term)"대신 "Section"에서 정의 증거에. (아마도마다 "설정"때문에 추가 시간에도 빈 확인합니다. 인쇄 할 수.)

어떻게 COQ을 가속화? (위의 항목에 오류가 있으면 내 연습에서 파생됩니다.)

계산의 가장 중요한 단계는 무엇이며 어떻게 처리해야합니까?

Answer 1

성배는 코드를 프로파일 링하고 핫스팟을 최적화하는 것입니다. Coq> = 8.6의 경우 전술 전략에 대해 Set Ltac Profiling. 및 Reset Ltac Profile. 및 Show Ltac Profile. 수 있습니다. -time 인수를 사용하여 coqc을 호출하면 줄 단위 타이밍 정보가 표시됩니다. sed 속임수의 비트가 당신을 위해 정보를 정렬 할 수 있습니다

는

coqc -time foo.v | sed s'/^\(.*\) \([0-9\.]\+ secs.*\)$/\2 \1/g' | sort -h 

COQ에서> = 8.8, 당신은 네이티브 컴파일러 프로파일 Set Native Compute Profiling 할 수있을 것입니다. 다른 병목 현상에 부딪혔다면, 추측에 능숙하거나 개발자에게 프로파일 링 도구를 추가하거나, 실행중인 coq 바이너리를 프로파일 링하거나, 코드를 프로파일 링 할 가치가 있다고 devs에게 확신시켜야합니다. (때로는 지연이 Coq의 효율성 버그를 가리킬 때 Pierre-Marie Pédrot에게 내 코드의 프로파일을 달 수 있습니다.)

한 가지 유용한 방법은 모든 커밋마다 코드를 항상 프로파일 링하는 것입니다. Coq> = 8.7의 경우 make-pretty-timed-before, make-pretty-timed-after 및 print-pretty-timed-diff이라는 대상이있어 파일 당 컴파일 시간이 서로 다른 두 가지 상태간에 diff 테이블을 정렬 할 수 있습니다. make TIMING=before, make TIMING=after, make all.timing.diff을 사용하면 회선 당 정보를 얻을 수 있습니다.

는 또한 Experience Implementing a Performant Category-Theory Library in Coq (자세한 미디어 here)을보고 관심이, 그리고 그 종이 (pdf) (pptx with presenter notes)의 프레젠테이션 아마 또한 슬라이드 갑판 수 있습니다.

---

당신이 언급 한 것들 중 대부분은 관련이 없지만 코퀴스는 여러 장소에서 느릴 수 있습니다.위해 당신을 통과 :

1. Theorem 및 Definition 동의어이며, 유일한 차이점은 Definition가 := 및 Theorem하지 않는 지원한다는 것입니다.
2. 더 나은 하드웨어, 더 많은 RAM, 빠른 CPU, 확실히 도움이되지만 Coq 용 최적화 컴파일러가 없습니다. 병렬 처리도 마찬가지입니다. 이 노트에서 파일 수준의 병렬 처리는 증명 수준의 병렬 처리보다 잘 작동하는 경향이 있습니다. 가능한 한 내 파일을 분할하고, 라이브러리 로딩 시간이 문제가되지 않도록 세분화 된 가져 오기를 사용하고 make -j을 사용하는 경향이 있습니다.
3. 모든 인수를 채우는 것이 도움보다 상처를 입힐 가능성이 큽니다. 특히 통념을 채우는 조건이 큰 경우 통일 비용이 추가로 발생합니다. 논쟁을 채워서하는 진정한 일은 통일에 반대하는 에바 창조를 교환하는 것입니다. 통일은 대개 느립니다. 그러나 표준 구조체 해상도, typeclass 해상도로 채워지거나 다른 역 추적 및 전개 또는 유니버스 변수 새로 고치기가 필요한 구멍이있는 경우이를 채워 넣으면 많은 작업이 빨라질 수 있습니다.
4. 증명 스크립트의 세미콜론과 마침표 사이의 차이점은 대화 형 모드 (coqtop/CoqIDE/ProofGeneral/etc에서 make을 실행하지 않을 때)에서만 중요하다고 생각합니다. 테스트하고 다른 방법을 발견하면 알려주세요.
5. 이것은 사실이며 인쇄 및 기타 작업에 모두 영향을줍니다. set 자체는 인쇄로 인해 느리지는 않지만 그 대신 목표의 모든 항목을 찾습니다 (어리석게도 약간 감소 (베타 - 이타? 기억이 안납니다), 오히려 문법적 평등보다 더), 새로운 가설로 바꿔라. 이 동작이 필요하지 않으면 set 대신 pose을 사용하십시오. 또한 큰 컨텍스트 변수는 컨텍스트의 크기에 따라 달라지는 전술을 느리게 할 수 있으므로이 섹션에서는 Definition이 더 빠릅니다.
   • 좋은 추상화 장벽을 선택하고, 종교를 존중 : 일에

다른 생각 나는으로 실행했습니다. 당신은 추상화 장벽을 깰 때마다 땀과 눈물로 돈을 지불 할 것입니다. (좋은 추상화 장벽을 고르는 것은 엄청나게 어렵습니다. 일반적으로 기존 수학적 추상화 또는 발행 된 논문을 복사하여이 작업을 수행합니다. 나는 지난 5 년 동안 정확히 한 번 완전히 처음부터 좋은 추상화 장벽을 생성 할 수있었습니다. "C와 유사한 코드를 작성할 때 모든 함수는 인수로 하나의 튜플을 가져 와서 결과로 하나의 튜플을 반환한다는"통찰력 "으로 설명 될 수 있습니다.)

반사 형 교정을 수행하는 경우 , 좋은 알고리즘을 선택하십시오. 단항 자연수를 사용하거나 알고리즘의 실행 시간이 지수 함수이면 증명 속도가 느려집니다.

Coq < 8.7에서 evar-map 정규화는 대량의 오버 헤드를 발생시킵니다.

느림 End Section (때로는 느림 : Defined)은 자주 rehashconsing에 대한 문제로 인해 발생합니다. 피어 - 마리는 EConstr 브랜치로이 문제를 해결했습니다. 이 문제를 해결하려면 손가락을 엇갈리게하고기도하십시오. (또는 Coq 개발자가되어 Coq을 수정하십시오.)

큰 몸체가있는 베어 fix을 검사 할 때 guardedness checker가 매우 느립니다 (베타 - iota-zeta reduxes가있는 상태에서만 가능할 수 있습니다). 해결 방법은 본문을 별도의 정의로 추출하는 것입니다.예를 들어,보다는 당신이

 
Definition length_step 
      (length : forall A, list A -> nat) 
      A (ls : list A) 
    : nat 
    := match ls with 
     | nil => 0 
     | cons _ xs => S (length _ xs) 
     end. 
Fixpoint length A (ls : list A) : nat 
    := length_step length A ls. 

• 이 COQ이 자유롭게 (때로는 일관성) 인라인 let x := ... in ... 문을 쉽게 지수 정의 국제화 시간으로 이어질 수있는 것이다주의하십시오 쓸 수

 
Fixpoint length A (ls : list A) : nat := 
    match ls with 
    | nil => 0 
    | cons _ xs => S (length _ xs) 
    end. 

를 작성 .

구체화를 수행 할 때 표준 구조는 빠르지 만 읽기 어렵습니다. Ltac은 약 2 배 느리고 typeclass 해상도는 2 배 느려질 수 있습니다 (또는 Ltac Reification과 동일한 속도 일 수 있음). 잘하면 Ltac2가 끝나면 상황이 나아질 것입니다.

simpl 큰 용어

내가 다시 와서 나중에 더 추가 (나를 추가 할 코멘트에 일을 제안 주시기) 수에 매우 느리지 만,이 반 괜찮은 시작이다.