GitHub - vllm-project/vllm: A high-throughput and memory-efficient inference and serving engine for LLMs
| Documentation | Blog | Paper | Discord | Twitter/X | Developer Slack | Latest News 🔥 [2024/12] vLLM joins pytorch ecosystem! Easy, Fast, and Cheap LLM Serving for Everyone! [2024/11] We hosted the seventh vLLM meetup with Snowflake! Please find the meetup slides from vLLM team here, and Snowflake team here. [2024/10] We have just created a developer slack (slack.vllm.ai) focusing on coordinatin
『OpenSSLクックブック』
コマンドラインでOpenSSLを使うすべての人に！ 『プロフェッショナルTLS&PKI』 からOpenSSLに関する章の全体を抜粋した無償のPDFミニブック！ Ivan Ristić 著、齋藤孝道 監訳 84ページ B5判 電子書籍の形式：PDF ISBN：N/A 2024年4月24日 第2版第1刷（原書Third Edition対応） 発行 安全なインターネットにとって必要不可欠なTLSプロトコルの詳細だけでなく、それを実世界で利用するために必要なエコシステムの成り立ちと全体像が丁寧に解説された ‟Bulletproof TLS and PKI”（Ivan Ristić著） の全訳 『プロフェッショナルTLS&PKI』 から、「第12章 OpenSSL」と「第13章 OpenSSLを使った動作検証」を抜粋した小冊子です。電子書籍のみの提供になります。
ProVerif
ProVerif: Cryptographic protocol verifier in the formal model ProVerif is an automatic cryptographic protocol verifier, in the formal model (so called Dolev-Yao model). This protocol verifier is based on a representation of the protocol by Horn clauses. Its main features are: It can handle many different cryptographic primitives, including shared- and public-key cryptography (encryption and signat
Coccinelle: A Program Matching and Transformation Tool for Systems Code
What is Coccinelle? Coccinelle is a program matching and transformation engine which provides the language SmPL (Semantic Patch Language) for specifying desired matches and transformations in C code. Coccinelle was initially targeted towards performing collateral evolutions in Linux. Such evolutions comprise the changes that are needed in client code in response to evolutions in library APIs, and
モダンCMake入門 - /home/tnishinaga/TechMEMO
CやC++などのビルドのための仕組みを持たない言語で書かれた大規模なコードをビルドする際、とくに複数の環境でのビルドが必要な場合はCMakeなどのビルドシステムジェネレレーターとNinjaなどのビルドシステムを用います。 この記事ではそういったところで使うCMakeのモダンな書き方について紹介します。 この記事の目的 この記事を通して少しでもモダンCMakeが書ける人が増えたり、世の中のビルドで悩む人が少しでも減らせたら嬉しいです。 TL;DR モダンCMakeは難しいのでChatGPTとかLLMと相談しながら書くのがオススメ 目次 この記事の目的 TL;DR 目次 モダンCMakeとは モダンCMakeの具体例 実行バイナリtargetの追加 ライブラリターゲットの追加 ターゲット間のリンクと伝搬設定 ターゲットのinclude設定 モダンCMakeのbest practice 非推奨設
Functional Programming in Lean - Functional Programming in Lean
Functional Programming in Lean by David Thrane Christiansen Copyright Microsoft Corporation 2023 This is a free book on using Lean 4 as a programming language. All code samples are tested with Lean 4 release 4.1.0. Release history January, 2024 This is a minor bugfix release that fixes a regression in an example program. October, 2023 In this first maintenance release, a number of smaller issues w
What is Lean - Lean Documentation Overview
What is Lean Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. Lean programming primarily involves defining types and functions. This allows your focus to remain on the problem domain and manipulating its data, rather than the details of programming. -- Defines a function that takes a name an
Theorem Proving in Lean 4 - Theorem Proving in Lean 4
by Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, with contributions from the Lean Community This version of the text assumes you’re using Lean 4. See the Quickstart section of the Lean 4 Manual to install Lean. The first version of this book was written for Lean 2, and the Lean 3 version is available here.
Theorem Proving in Lean 4 日本語訳 - Theorem Proving in Lean 4 日本語訳
Theorem Proving in Lean 4 by Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, with contributions from the Lean Community このテキストは読者がLean 4を使うことを前提にしています。Lean 4をインストールするには、Lean 4 Manualの節Quickstartをご覧ください。このテキストの最初のバージョンはLean 2用に書かれました。Lean 3用のバージョンはこちらで入手可能です。 この翻訳について translated by aconite(2章～12章), Haruhisa Enomoto(1章) この翻訳は有志による非公式翻訳です。翻訳に際して、表現を大きく変えた箇所や、分かりやすさを期すため記述やコード例を追加
アプリ開発者のにとっての Tauri v2 のセキュリティ構造を読み解く - Qiita
はじめに Tauri v2 にバージョンが上がり、モバイル (iOS/Android) 対応が正式にサポートされた。 また、プラグインに関して大幅なサポート変更があり、Tauri のコア部分までアクセスできるものを作成できるようになった。 そして、Tauri v1 の学びから、高度なセキュリティサポートが明確になっていき、こうして Tauri v2 のセキュリティサポートは大幅な変更と対応拡張が行われたという経緯がある。 公式ドキュメント まずは公式ドキュメントをぺたり。 これを読み解きつつ、特に注意したり、自分が使うときにどう設定すればいいかを考えながらまとめていく。 トラスト境界 (Trust Boundaries) を意識する トラスト境界 (Trust Boundaries/トラストバウンダリ) は、プログラムデータや実行が「信頼」のレベルを変更する境界、または異なる機能を持つ2つ
Neovimはじめてみた
TerminalにはWezTermを使用しています。使い始めたのは最近ですが、設定をテキストファイルで管理できる点がとても良いです。以前はiTerm2を使用しており、ストレスはなかったのですが、今ではWezTermの方が良いと考えています。 コーディングで主に使用しているのはJetBrainsのIDE（PyCharm、WebStorm、PhpStorm）です。JetBrainsのIDEは、デフォルトで各種言語の補完が効き、プラグインを追加しなくてもストレスなくコーディングできる点が優れています。また、JetBrainsにプラグインの追加は控えめにしています。プラグインの追加はGUIベースとなるため、管理が煩雑になることと、異なる環境間での共有が難しいためです。もちろん、設定のエクスポート機能を使用できますが、設定を変更するたびにエクスポート・インポートを行うのは煩わしいためです。 VSCo
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - flux-rs/flux: Refinement Types for Rust
GitHub - ocamllibs/clangml: OCaml bindings for Clang
https://www.cs.princeton.edu/~appel/papers/plcc.pdf
GitHub - argumentcomputer/Megaparsec.lean: Lean 4 port of Megaparsec
Learning Lean 4
GitHub - leanprover-community/mathlib4: The math library of Lean 4
「Plurality」とは何か｜日本語版解説
RunPod - The Cloud Built for AI
GitHub - amitds1997/remote-nvim.nvim: Remote development in Neovim 🔥
