Skip to content

Instantly share code, notes, and snippets.

@asi1024 asi1024/TopProver.md Secret
Last active Nov 5, 2019

Embed
What would you like to do?

TopProver Q&A

  1. Q: 自動証明タクティックを使っても良いですか? A: 標準ライブラリの範囲ならOKです

  2. Q: Source code policy とは何ですか? A: ユーザの提出コードを公開するか、非公開にするかの設定です。 (コンテスト中は Private に設定されていても、コンテスト終了後に Public になることがあります。)

  3. Q: SSReflect 使いたいです A: Require Import ssreflect で使えます。MathComp 1.9.0 も最近入れました

  4. Q: Pretest とは何ですか? A: このジャッジシステムでは、作題者の認めていない公理 (Admitted してる、など) を coqchk を用いて利用しているのですが、 coqchk の実行には時間がかかるので、ジャッジを Pretest (coqc のビルドが通るかどうか) と System Test (coqchk によるチェック) の 2 段階に分け、 Pretest を優先的に実行するようにしています。変なことをしていない限りは基本的に Pretest が通れば System Test も通ります。(具体的には、 Problem.vSolution.v の Axiom の diff をチェックしています。 Problem.v で認めている公理は用いても OK です。)

  5. Q: コンテストの日程がいつの間にか変わっているようです A: 競技プログラミングと参加者層が近いので、その時間帯に競技プログラミングのコンテスト (AtCoder, Codeforces 等) がある場合は、告知なく日程や開始時刻を変更する可能性があります。ご容赦くださいm(_ _)m。

  6. Q: Ratingとは何ですか? A: (TODO)

その他

  • 最近ドメイン取りました: https://top-prover.top/#
  • 作題者募集してます
  • カレンダー
  • 質問や要望等あれば連絡ください: https://twitter.com/asi1024
  • 最近忙しくて次のコンテストを準備する余裕がないです。すみません。
    • 問題案を募集しています。出題者が現れ次第次のコンテストを開催します。

ここ最近の気持ち

  • 計算量上限を証明する問題など出して競技プログラミングから参加者層を引き抜きたいなあと思っている
    • これ の 3.3 節とか使えそうかなあ、とちょっと思ってる
    • 定義を書いてみたけど結構重くなってしまったので、コンテストには不向きかもしれない
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.