守株阁

Gallina 是 Coq 的规范语言（specification language），负责定义类型、函数和命题；tactic 语言（Ltac/Ltac2）只是证明搜索的外壳，最终生成的证明项本质上仍是 Gallina 表达式。本篇是一张速查表，覆盖 Definition、Fixpoint、Inductive、Record、Section、Module 六个核心构造，以及模式匹配、匿名函数、隐式参数的基本用法，目标是让读者能独立写出完整的 .v 文件并通过 coqc 零 warning 编译。前置阅读：形式化方法系列《归纳类型与递归——把数据嵌入证明》和《依值类型——从命题逻辑到一阶逻辑》。 Definition Definition 引入一个全局名称，绑定到一个 Gallina 表达式。类型标注可选；省略时 Coq 从右侧推断。 12345678(* 带类型标注 *)Definition double : nat -> nat := fun n => n + n.(* 省略类型标注，Coq 推断 *)Definition triple n := n + n + n...

Coq 的证明过程不是一次性写出完整的证明项，而是通过 tactic 序列逐步缩减待完成的工作。每执行一条 tactic，Coq 会更新"当前需要证明的内容"，直到不再有任何待证目标，Qed 才能通过。这个状态驱动的交互过程有一个专用的视图——目标窗口（goal window）。 证明状态机 每个 Proof. 之后，Coq 内部维护一个证明状态（proof state），其结构是一个目标列表，每个目标由两部分组成： 123context (上下文 / 假设区)━━━━━━━━━━━━━━━━━━━━━━━━━━goal (当前要证明的命题) 在 CoqIDE 或 VS Code vscoq2 插件里，这个结构对应右侧的 Goals 面板。在 Proof General (Emacs) 里，它出现在 *goals* 缓冲区。在命令行 coqtop 里，每执行完一条 tactic 后，Coq 打印出更新后的状态。 分隔符 ============================ 是可视化的 ⊢ 符号。分隔符上方是已知假设，下方是当前目标。 一个典型的中间状态（...

「形式化方法」系列的 14 篇文章建立了 Curry-Howard 同构、依值类型、归纳类型与 Lean 4 入门的理论底座。本系列从工具链入手，目标是让读者能独立用 Coq 完成 200 行以内的证明项目。本篇处理的问题只有一个：从零搭建一套可重复、可在 CI 上运行的 Coq 开发环境。 opam switch 管理 Coq 的工具链通过 opam 管理，opam 是 OCaml 生态的包管理器。Coq 8.20 要求 OCaml ≥ 4.09（coq-core.opam 里写的是 "ocaml" {>= "4.09.0"}），4.x 系列官方测试到 4.14.1，OCaml 5.x 支持仍标注为实验性——所以下面固定用 4.14.2。不同项目可能需要不同的 Coq 版本，因此每个项目建议使用独立的 opam switch。 本系列锚定 Coq 8.20，因为它是存量项目的公共分母。但要先说清一件事：Coq 在 8.20 之后更名为 Rocq，现在 opam install coq 装到的可能是 9.x 的兼容层。9.0 起标准...

大规模图计算是互联网基础设施的重要组成部分。社交网络中的好友关系、金融风控中的资金流转链路、供应链中的货品追溯，本质上都是图结构问题。本文专注计算范式、批量与增量引擎、规模化算法和基准测试；图数据库、知识图谱与 GNN 的全链路地图见《深入图工程》，Agent 编排中的图模型则由《Coding Agent 领域的 Graph Engineering》展开。 图计算范式 Pregel 与 BSP 模型 2010 年，Google 在 SIGMOD 发表 Pregel 论文，确立了大规模图计算中影响深远的"以顶点为中心"（vertex-centric）编程抽象。开发者实现单个顶点的计算逻辑，系统负责分区、消息传递和全局协调。 执行单元是超步（superstep）：所有活跃顶点先并行执行用户定义的 compute() 函数，顶点通过消息向邻居传递结果，消息在超步间缓冲；当前超步内所有顶点计算完毕后进行全局屏障同步，再进入下一超步。 这是 Leslie G. Valiant 在 1990 年提出的 BSP（Bulk Synchronous Parallel）模型在图...

图（Graph）作为数据结构，在计算机科学里存在了半个多世纪。“图工程”（Graph Engineering）并不是边界明确的正式学科名称，本文把它作为一个工作定义：围绕图的建模、存储、查询、计算、学习、运维与验证形成的系统工程。图规模、消费者和时效性要求扩大之后，这些原本分散的工作需要放进同一套方法中讨论。 图工程的学科定位 图工程在本文中承载两层含义。第一层是以图数据为中心的系统工程，涵盖建模、存储、查询、计算和学习全链路。第二层来自 AI Agent 领域：有些框架直接采用有向状态图，有些采用 crew、conversation、handoff 或普通工作流抽象；"图"是分析这些编排关系的统一视角，但并非每个框架的字面核心。两层含义的交叉点是 Agent 以知识图谱或代码图作为上下文源。计算引擎的细节见《图工程综述》，Agent 编排的边界见《Coding Agent 领域的 Graph Engineering》。 与传统数据工程的关键分野在于： 分区目标通常难以精确求解。关系型数据常按主键 hash 或 range 分片；图分区需要同时考虑负载、割边...

Unix 常用命令全景指南 本文系统梳理 Unix/Linux 环境下的高频命令，从命令行语法基础到生产环境实战，覆盖文件操作、文本处理、系统监控、开发工具四大场景。 目录 命令行基础 文件与目录操作 文本处理三剑客 系统与资源监控 开发环境工具链 磁盘告警定位实战 磁盘扩容实战 命令行基础 命令行参数的三元素 Unix 命令行由三种基本元素组成：选项、位置参数和子命令。 基本结构 1command [options] [positional_arguments] 选项（Options） 以 - 或 -- 开头的参数，用于修改命令行为： 类型 格式 示例 短选项 - + 单个字母 -a, -v, -h 长选项 -- + 单词 --help, --verbose 带参数的选项 -n value 或 --name=value -n namespace, --port=8080 短选项支持合并书写：ls -la 等价于 ls -l -a。 位置参数（Positional Arguments） 不带连字符的参数，其含义由出现的位置决定： 123cp so...

上一篇把 Logstash 和 Fluentd、Vector 放在一起横向对比。这一篇转向纵向：Logstash 自 2009 年诞生以来历经哪些关键演进，Elastic Agent 和 OpenTelemetry Collector 的出现又如何重新划定了它的边界。 核心问题：持久队列、DLQ、pipeline-to-pipeline 一路补齐的是什么——当 Elastic Agent 分走了边缘采集场景、OTel 提供了厂商中立的替代方案，Logstash 今天的定位是什么。 本篇的版本坐标截至 2026-08：Logstash 的最新发布版本是 9.5.2，8.19 分支仍在维护。下面时间线里每一行的版本归属，取自官方 release notes 的原文，或该功能文档在各发布分支上的首次出现；发布日期取自对应 tag 的提交时间。全系列统一的版本前提见第 01 篇。 演进时间线 123456789101112131415161718版本 发布 关键变化───────────────────────────────────────────────────────...

上一篇厘清了 Logstash、Beats、Ingest Pipeline 在 Elastic Stack 内部的分工。这一篇跳出 Elastic 生态，把 Logstash 和来自 CNCF 生态的 Fluentd 以及 Rust 实现的 Vector 放在一起比较，回答一个跨生态的架构选择问题。 核心问题：三者在插件生态、资源占用、性能、可靠性这四个维度上各自取了什么——JVM 系与原生系的根本差异体现在哪里，什么场景下差异会决定选型。 三方现状以 Logstash 9.5.x、Fluentd v1、Vector v0.57 为准，插件/组件计数与仓库活跃度取自 2026-08。跨生态对比的时效性衰减比机制类内容快得多，所以下面每个量化断言都标了统计口径和取数来源，便于日后自己重新核一遍。全系列统一的版本前提见第 01 篇。 三者的基本参数 12345工具 语言运行时 开源年份 归属──────────────────────────────────────────────────Logstash JVM + JRuby 20...

上一篇讲完了性能调优的系统方法。这一篇进入演进对比阶段，把 Logstash、Beats 和 Elasticsearch Ingest Pipeline 三者并排放，回答一个工程决策问题：同样是把数据搬进 ES，三种路径在哪里分叉，分叉的依据是什么。 核心问题：轻量采集用 Beats，简单解析下沉到 Ingest Pipeline，复杂转换才留给 Logstash——这条分工逻辑背后的资源、能力和可靠性代价是什么？ 本篇的三方现状以 Logstash 9.5.x、Elasticsearch 8.19/9.x 的 ingest 文档、Filebeat 与 Elastic Agent 9.x 为准，数据取自 2026-08。全系列统一的版本前提见第 01 篇。 三者的定位 Elastic Stack 的数据接入层有三个层次，各自定位不同： 123456789101112数据源 │ ├─▶ [Beats / Elastic Agent] Go 语言，轻量级进程，低资源 │ │ Beats 单一职责；Agent 单进程整合多...

上一篇解决了怎么用 Node Stats API 和 hot threads 定位瓶颈在哪一段。这一篇进入调优执行层：拿到瓶颈定位结论之后，heap 大小、GC 策略、batch 与 worker 组合、持久队列磁盘 I/O 各应该怎么调。 核心问题：heap 大小与 GC 停顿之间的取舍；pipeline.workers 与 pipeline.batch.size 的组合效果；持久队列磁盘成为瓶颈时的判断和处置。 调优对象全景 1234567891011121314151617181920212223242526 调优旋钮分布图┌────────────────────────────────────────────────────────┐│ JVM 层 ││ heap size (jvm.options: -Xms / -Xmx) ││ off-heap (PQ mmap page / direct memory / 线程栈) ...