Skip to content
Permalink

Comparing changes

This is a direct comparison between two commits made in this repository or its related repositories. View the default comparison for this range or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: coq/rocq-prover.org
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: 4609bbf5f49484664c3d8e19cbc1e5904f7e6db9
Choose a base ref
..
head repository: coq/rocq-prover.org
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: 90f11b08fdbbd7c5fc193d43ee3f93bec066f497
Choose a head ref
1 change: 0 additions & 1 deletion .dockerignore
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
*
!rocq-doc/
!asset/
!data/
!src/
6 changes: 3 additions & 3 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
@@ -58,6 +58,6 @@ jobs:
- name: Run tests
run: opam exec -- dune test

- name: Format code
run: opam exec -- dune build --auto-promote @fmt
if: runner.os == 'Linux'
# - name: Format code
# run: opam exec -- dune build --auto-promote @fmt
# if: runner.os == 'Linux'
4 changes: 2 additions & 2 deletions .github/workflows/generate-logos.yml
Original file line number Diff line number Diff line change
@@ -9,7 +9,7 @@ jobs:

steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v4
- name: Create zip file rocq-logos.zip
run: |
if [ -d "rocq-id/avatar" ] && [ -d "rocq-id/badges" ] && [ -d "rocq-id/logos" ] && [ -f "rocq-id/ROCQ_ID-guidelines.pdf" ]; then
@@ -28,6 +28,6 @@ jobs:
git add rocq-id/rocq-logos.zip
git commit -m "Add zipped rocq-logos folder"
- name: Push changes
uses: ad-m/github-push-action@v0.6.0
uses: ad-m/github-push-action@v0.8.0
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
3 changes: 0 additions & 3 deletions .gitmodules
Original file line number Diff line number Diff line change
@@ -1,3 +0,0 @@
[submodule "rocq-doc"]
path = rocq-doc
url = https://github.com/coq/doc
3 changes: 1 addition & 2 deletions Dockerfile
Original file line number Diff line number Diff line change
@@ -33,7 +33,6 @@ RUN chmod -R 755 /var
COPY --from=build /home/opam/package.state /var/package.state
COPY --from=build /home/opam/rocq-opam-repository /var/opam-repository
COPY --from=build /home/opam/_build/default/src/rocqproverorg_web/bin/main.exe /bin/server
COPY --from=build /home/opam/rocq-doc /doc

COPY playground/asset playground/asset

@@ -47,4 +46,4 @@ ENV ROCQPROVERORG_HTTP_PORT=8080

EXPOSE 8080

ENTRYPOINT /bin/server
ENTRYPOINT [ "/bin/server" ]
6 changes: 4 additions & 2 deletions LICENSE
Original file line number Diff line number Diff line change
@@ -4,7 +4,9 @@ Licenses
- Content is released under CC BY-SA 4.0.
- Code that implements the various tools in this repository is released under the ISC license.
- Code examples within content are released under the UNLICENSE.
- Design of the site. All rights reserved by the rocq-prover.org project.
- Design of the site. The website is an overhaul of the OCaml.org design,
whose rights are reserved by the OCaml.org project (http://github.com/ocaml/ocaml.org).
For the new design, All rights are reserved by rocq-prover.org project.
- Rocq logo is released under the UNLICENSE.
- Abstracts, slides from meetings. Rights retained by contributor.

@@ -68,7 +70,7 @@ For more information, please refer to <https://unlicense.org/>
* ISC

ISC License (ISC)
Copyright (c) 2021, rocq-prover.org project
Copyright (c) 2021, OCaml.org project

Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted, provided that the above copyright notice and this permission notice appear in all copies.

17 changes: 13 additions & 4 deletions Makefile
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
.DEFAULT_GOAL := all
DOC_PATH=`pwd`/rocq-doc/

.PHONY: all
all:
@@ -32,8 +33,18 @@ playground:
install: all ## Install the packages on the system
opam exec -- dune install --root .

.PHONY: local-doc
local-doc:
if [ -d rocq-doc ]; then cd rocq-doc && git pull; \
else git clone --depth 1 https://github.com/coq/doc.git rocq-doc; fi

.PHONY: update-local-doc
update-local-doc:
@if [ -d rocq-doc ]; then cd rocq-doc && git pull; \
else echo "No local doc copy, use \"make local-doc\" to get a local copy (~ 8 GB)"; fi

.PHONY: start
start: all ## Run the produced executable
start: all update-local-doc ## Run the produced executable
opam exec -- dune exec src/rocqproverorg_web/bin/main.exe

.PHONY: test
@@ -51,11 +62,9 @@ doc: ## Generate odoc documentation
.PHONY: fmt
fmt: ## Format the codebase with ocamlformat
opam exec -- dune build --root . --auto-promote @fmt

DOC_PATH=`pwd`/rocq-doc/

.PHONY: watch
watch: ## Watch for the filesystem and rebuild on every change
watch: update-local-doc ## Watch for the filesystem and rebuild on every change
DOC_PATH=${DOC_PATH} opam exec -- dune build @run -w --force --no-buffer

.PHONY: utop
11 changes: 11 additions & 0 deletions compose.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
services:
web:
restart: always
build: .
ports:
- "127.0.0.1:8000:8080"
volumes:
- type: bind
source: ${DOC_PATH}
target: /doc
read_only: true
6 changes: 3 additions & 3 deletions data/books/mathcomp.md
Original file line number Diff line number Diff line change
@@ -5,7 +5,7 @@ description: >
Mathematical Components is the name of a library of formalized mathematics for the Coq proof assistants. It covers a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to more advanced results in various flavors of algebra.
recommendation: >
Mathematical Components is the name of a library of formalized mathematics for the Coq proof assistants. It covers a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to more advanced results in various flavors of algebra. This library constitutes the infrastructure for the machine checked proofs of the Four Color Theorem and of the Odd Order Theorem.
This book aims at providing an introducing to the design patterns used throughout this library, so as to ease its use for other projects. While there are several books around covering the usage of the Coq system and the theory it is based on, the Mathematical Components library uses a few design patterns that differ from the methodology propose in other sources. As a consequence, this book provides a slightly non-standard presentation of Coq, putting upfront the formalization choices and the proof style that are the pillars of the library.
This book aims at providing an introducing to the design patterns used throughout this library, so as to ease its use for other projects. While there are several books around covering the usage of the Coq system and the theory it is based on, the Mathematical Components library uses a few design patterns that differ from the methodology proposed in other sources. As a consequence, this book provides a slightly non-standard presentation of Coq, putting upfront the formalization choices and the proof style that are the pillars of the library.
This books targets two natures of audience. On one hand newcomers, in particular beginners with background in mathematics rather than computer science, should find a soft introduction to the programming language of Coq, Gallina, and to the Ssreflect proof language. On the other hand, accustomed Coq users will find a substantial account of the formalization style that made the Mathematical Components library possible.
authors:
- Assia Mahboubi
@@ -17,15 +17,15 @@ language:
links:
- description: Read Online
uri: https://math-comp.github.io/mcb/
difficulty: intermediate
difficulty: beginner
pricing: free
---



Mathematical Components is the name of a library of formalized mathematics for the Coq proof assistants. It covers a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to more advanced results in various flavors of algebra. This library constitutes the infrastructure for the machine checked proofs of the Four Color Theorem and of the Odd Order Theorem.

This book aims at providing an introducing to the design patterns used throughout this library, so as to ease its use for other projects. While there are several books around covering the usage of the Coq system and the theory it is based on, the Mathematical Components library uses a few design patterns that differ from the methodology propose in other sources. As a consequence, this book provides a slightly non-standard presentation of Coq, putting upfront the formalization choices and the proof style that are the pillars of the library.
This book aims at providing an introducing to the design patterns used throughout this library, so as to ease its use for other projects. While there are several books around covering the usage of the Coq system and the theory it is based on, the Mathematical Components library uses a few design patterns that differ from the methodology proposed in other sources. As a consequence, this book provides a slightly non-standard presentation of Coq, putting upfront the formalization choices and the proof style that are the pillars of the library.

This books targets two natures of audience. On one hand newcomers, in particular beginners with background in mathematics rather than computer science, should find a soft introduction to the programming language of Coq, Gallina, and to the Ssreflect proof language. On the other hand, accustomed Coq users will find a substantial account of the formalization style that made the Mathematical Components library possible.

Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
---
title: "Programs and Proofs: Mechanizing Mathematics with Dependent Types"
slug: "mechanized-rocq"
slug: "programs-and-proofs"
description: >
These lecture notes are the result of the author's personal experience of learning how to structure formal reasoning using the Rocq Prover and employ Rocq in large-scale research projects. The present manuscript offers a brief and practically-oriented introduction to the basic concepts of mechanized reasoning and interactive theorem proving.
recommendation: >
@@ -14,12 +14,12 @@ language:
links:
- description: Read Online
uri: https://ilyasergey.net/pnp/
difficulty: intermediate
difficulty: beginner
pricing: free
---

These lecture notes are the result of the author's personal experience of learning how to structure formal reasoning using the Rocq Prover and employ Rocq in large-scale research projects. The present manuscript offers a brief and practically-oriented introduction to the basic concepts of mechanized reasoning and interactive theorem proving.

The primary audience of the manuscript are the readers with expertise in software development and programming and knowledge of discrete mathematic disciplines on the level of an undergraduate university program. The high-level goal of the course is, therefore, to demonstrate how much the rigorous mathematical reasoning and development of robust and intellectually manageable programs have in common, and how understanding of common programming language concepts provides a solid background for building mathematical abstractions and proving theorems formally. The low-level goal of this course is to provide an overview of the Rocq Prover, taken in its both incarnations: as an expressive functional programming language with dependent types and as a proof assistant providing support for mechanized interactive theorem proving.

By aiming these two goals, this manuscript is, thus, intended to provide a demonstration how the concepts familiar from the mainstream programming languages and serving as parts of good programming practices can provide illuminating insights about the nature of reasoning in Rocq's logical foundations and make it possible to reduce the burden of mechanical theorem proving. These insights will eventually give the reader a freedom to focus solely on the essential part of the formal development instead of fighting with the proof assistant in futile attempts to encode the "obvious" mathematical intuition.
By aiming these two goals, this manuscript is, thus, intended to provide a demonstration how the concepts familiar from the mainstream programming languages and serving as parts of good programming practices can provide illuminating insights about the nature of reasoning in Rocq's logical foundations and make it possible to reduce the burden of mechanical theorem proving. These insights will eventually give the reader a freedom to focus solely on the essential part of the formal development instead of fighting with the proof assistant in futile attempts to encode the "obvious" mathematical intuition.
33 changes: 33 additions & 0 deletions data/books/sf-zh.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
---
title: "《软件基础》中译版"
slug: "sf-zh"
description: >
《软件基础》系列广泛地介绍了可靠软件的数学基础。
recommendation: >
《逻辑基础》为本系列书籍的切入点。它涵盖了函数式编程、逻辑的基本概念、计算机辅助定理证明以及 Rocq 证明助理。
《编程语言基础》考察了编程语言理论,包括操作语义、霍尔逻辑以及静态类型系统。
《函数式算法验证》展示了如何对各种基础数据结构进行机器验证。
《QuickChick:用 Rocq 进行基于性质的测试》介绍了将随机化基于性质的测试与 Rocq 生态系统中的形式化规范和证明相结合的工具和技术。
authors:
- Benjamin C. Pierce
- and many others
published: 2024-08-25
cover: books/sf-1.jpg
language:
- chinese
links:
- description: Read Online
uri: https://coq-zh.github.io/SF-zh/
difficulty: beginner
pricing: free
---

**《软件基础》系列广泛地介绍了可靠软件的数学基础。**

本系列书籍最主要的新颖之处在于,书中的每一处细节都百分之百地形式化且通过了机器验证。每卷书中的所有文本,包括练习,都是一份 Rocq 证明助理的「证明脚本」。

本系列书籍的目标受众包括从高年级本科生到博士以及研究者在内的广大读者。书中并未假定读者有逻辑学或编程语言的背景,不过一定的数学熟练度会很有帮助。
1. 《逻辑基础》为本系列书籍的切入点。它涵盖了函数式编程、逻辑的基本概念、计算机辅助定理证明以及 Rocq 证明助理。
2. 《编程语言基础》考察了编程语言理论,包括操作语义、霍尔逻辑以及静态类型系统。
3. 《函数式算法验证》展示了如何对各种基础数据结构进行机器验证。
4. 《QuickChick:用 Rocq 进行基于性质的测试》介绍了将随机化基于性质的测试与 Rocq 生态系统中的形式化规范和证明相结合的工具和技术。
Loading