Pin Aeneus in `lakefile.lean` in SymCRust
まだ誰も着手していません。
評価
- 難易度
- 1/5
- 見積もり時間
- 1時間未満
- 初心者へのやさしさ
- 85/100
- issue の種類
- リファクタリング
- 明瞭さ
- 明確に書かれている
- 活発さ
- 静か
- 技術スタック
- git
- 領域
- build-system
調査の方向性
依存関係の設定は、リンク先の行にある SymCRust/lean/lakefile.lean にあります。そこから始め、Issue に示されている明示的な Aeneas git 要件と、兄弟ディレクトリの配置を比較してください。コミット d71d2e3f とパス backends/lean を使用し、その後、Lean プロジェクトが宣言から Aeneas を解決することを確認してください。
索引モデルが issue の本文から書いたものです。
説明
Currently, aeneas is expected to be in a sibling directory and pinned to d71d2e3f.
However, aeneas can be explicitly pinned in the lakefile.lean by doing
require aeneas from git
"https://github.com/AeneasVerif/aeneas" @ "d71d2e3f2cb763f7faf15ab606ac9cf32da8dead" / "backends/lean"
Disclosure: I am interested in using this repository to mine Lean4 proving challenges for evaluating and training LLMs, which I would like to publish to HuggingFace as open source. This change will make running these evaluations a little more turnkey.
- 主要言語
- C
- スター
- 890
- フォーク
- 91
- PR マージ指標
- 30日以内にマージされた PR はありません
コントリビューションガイド
このリポジトリのコントリビューションガイドは索引されていません
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
microsoft/SymCrypt のほかの issue
-
bug compiler-support
難易度 4/5 3〜5日 初心者へのやさしさ 42/100
-
enhancement
難易度 5/5 1週間以上 初心者へのやさしさ 25/100
-
難易度 5/5 1週間以上 初心者へのやさしさ 25/100
-
難易度 5/5 1週間以上 初心者へのやさしさ 25/100
-
enhancement
難易度 5/5 1週間以上 初心者へのやさしさ 20/100
microsoft/SymCrypt の issue をすべて見る
似ている issue
-
bug
難易度 2/5 1〜3時間 初心者へのやさしさ 75/100
bradcypert/plum#53 ·
-
Component: GLib
難易度 2/5 1〜3時間 初心者へのやさしさ 70/100
-
難易度 2/5 1〜3時間 初心者へのやさしさ 75/100
-
Status: Opened
難易度 2/5 1〜3時間 初心者へのやさしさ 70/100
-
難易度 2/5 1〜3時間 初心者へのやさしさ 75/100
nextbsd/nextbsd-userland#285 ·