From ffc61b83cea660af250400ec9e72d939307066ab Mon Sep 17 00:00:00 2001 From: Jonas Kastberg Hinrichsen Date: Wed, 19 Jan 2022 16:44:07 +0100 Subject: [PATCH 01/10] Updated suggested indendation configurations --- docs/editor.md | 43 +++++++++++++++++++++++++++++++++---------- 1 file changed, 33 insertions(+), 10 deletions(-) diff --git a/docs/editor.md b/docs/editor.md index d59d4a550..a6eb9e05b 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -134,19 +134,42 @@ To solve some of these indentation errors you can add the following line to your initialisation file: ``` (setq coq-smie-user-tokens - '(("∗" . "*") - ("-∗" . "->") - ("∗-∗" . "<->") - ("==∗" . "->") - ("⊢" . "->") - ("⊣⊢" . "<->") - ("⋅" . "*") - (":>" . ":=") - ("by" . "now") - ("forall" . "now"))) + '(("," . ":=") + ("∗" . "->") + ("-∗" . "->") + ("∗-∗" . "->") + ("==∗" . "->") + ("=∗" . "->") ;; Hack attempt at matching ={E1,E2]=∗ + ("|==>" . ":=") + ("⊢" . "->") + ("⊣⊢" . "->") + ("↔" . "->") + ("←" . "<-") + ("→" . "->") + ("=" . "->") + ("==" . "->") + ("/\\" . "->") + ("⋅" . "->") + (":>" . ":=") + ("by" . "now") + ("forall" . "now") ;; NB: this breaks current ∀ indentation. + ("●" . "->") + ("◯" . "->") + ("●F" . "->") + ("◯F" . "->"))) ``` This will let the indentation strategy treat the Iris symbols (e.g. `-∗`) similar to the closely related Coq symbols (e.g. `->`). +Note that `->` is used in many places, which indent statements as: +``` + P * + Q +``` +as opposed to `∧`, which indents them as: +``` + P * + Q +``` ## CoqIDE 8.9 and earlier on Linux (ibus-m17n) -- GitLab From 1bb9d3f6459cb27a4ec330a1464b2c4f78aaed09 Mon Sep 17 00:00:00 2001 From: Jonas Kastberg Hinrichsen Date: Fri, 6 May 2022 14:39:38 +0200 Subject: [PATCH 02/10] Improved indentation configuration documentation --- docs/editor.md | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/docs/editor.md b/docs/editor.md index a6eb9e05b..292fa9dd2 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -160,15 +160,23 @@ initialisation file: ``` This will let the indentation strategy treat the Iris symbols (e.g. `-∗`) similar to the closely related Coq symbols (e.g. `->`). -Note that `->` is used in many places, which indent statements as: +Note that `->` is used in many places, as its indentation behaviour is: ``` - P * + P -> Q ``` -as opposed to `∧`, which indents them as: +This is the indentation behaviour is what we want, e.g. for `∗`: ``` - P * - Q + P ∗ + Q +``` +Note that this configuration has some caveats. +Notably, the change to `forall` (which gives good behaviour to e.g. +`iInduction xs as [|x xs IHxs] forall (ys).`), now gives the following indentation +behaviour to universal quantification: +``` + ∀ x, + P x ``` ## CoqIDE 8.9 and earlier on Linux (ibus-m17n) -- GitLab From f19892d93c5dfe9448a04532874c97f2f5d7409b Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 11 May 2022 11:21:48 +0000 Subject: [PATCH 03/10] Apply 1 suggestion(s) to 1 file(s) --- docs/editor.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/editor.md b/docs/editor.md index 292fa9dd2..b1e2cdffb 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -171,7 +171,7 @@ This is the indentation behaviour is what we want, e.g. for `∗`: Q ``` Note that this configuration has some caveats. -Notably, the change to `forall` (which gives good behaviour to e.g. +Notably, the change to `forall` (which gives good behavior to e.g. `iInduction xs as [|x xs IHxs] forall (ys).`), now gives the following indentation behaviour to universal quantification: ``` -- GitLab From 7962ba3d6d70d8b26d023214a56c725cbdf8c060 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 11 May 2022 11:22:06 +0000 Subject: [PATCH 04/10] Apply 1 suggestion(s) to 1 file(s) --- docs/editor.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/editor.md b/docs/editor.md index b1e2cdffb..9a4b585fe 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -173,7 +173,7 @@ This is the indentation behaviour is what we want, e.g. for `∗`: Note that this configuration has some caveats. Notably, the change to `forall` (which gives good behavior to e.g. `iInduction xs as [|x xs IHxs] forall (ys).`), now gives the following indentation -behaviour to universal quantification: +behavior to universal quantification: ``` ∀ x, P x -- GitLab From 98e2ee31cebfdacde8cadb16d4697b6095bad021 Mon Sep 17 00:00:00 2001 From: Jonas Kastberg Hinrichsen Date: Wed, 11 May 2022 13:23:34 +0200 Subject: [PATCH 05/10] Removed overly-specific indentation rules --- docs/editor.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/docs/editor.md b/docs/editor.md index 9a4b585fe..bd2c8831c 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -153,10 +153,6 @@ initialisation file: (":>" . ":=") ("by" . "now") ("forall" . "now") ;; NB: this breaks current ∀ indentation. - ("●" . "->") - ("◯" . "->") - ("●F" . "->") - ("◯F" . "->"))) ``` This will let the indentation strategy treat the Iris symbols (e.g. `-∗`) similar to the closely related Coq symbols (e.g. `->`). -- GitLab From a975355e3a2fad14a37dc1e5fdf546ac4f77f237 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 11 May 2022 13:35:52 +0000 Subject: [PATCH 06/10] clarify doc --- docs/editor.md | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/editor.md b/docs/editor.md index bd2c8831c..786b87919 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -174,6 +174,7 @@ behavior to universal quantification: ∀ x, P x ``` +This is not what we want; the second line should be indented by 2 spaces. ## CoqIDE 8.9 and earlier on Linux (ibus-m17n) -- GitLab From d04940a039b78df97521b9eb77d994011bafda71 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 11 May 2022 13:39:05 +0000 Subject: [PATCH 07/10] clarify comment --- docs/editor.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/editor.md b/docs/editor.md index 786b87919..cbe66683c 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -139,7 +139,7 @@ initialisation file: ("-∗" . "->") ("∗-∗" . "->") ("==∗" . "->") - ("=∗" . "->") ;; Hack attempt at matching ={E1,E2]=∗ + ("=∗" . "->") ;; Hack to match ={E1,E2]=∗ ("|==>" . ":=") ("⊢" . "->") ("⊣⊢" . "->") -- GitLab From 51d27ea4d2057c420e27f61169ed59daa66ce708 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 11 May 2022 13:40:35 +0000 Subject: [PATCH 08/10] fix typo --- docs/editor.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/editor.md b/docs/editor.md index cbe66683c..2077755d3 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -139,7 +139,7 @@ initialisation file: ("-∗" . "->") ("∗-∗" . "->") ("==∗" . "->") - ("=∗" . "->") ;; Hack to match ={E1,E2]=∗ + ("=∗" . "->") ;; Hack to match ={E1,E2}=∗ ("|==>" . ":=") ("⊢" . "->") ("⊣⊢" . "->") -- GitLab From 7d544510e1044403a5f52af1fce73f1c2fa830ec Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 11 May 2022 14:22:40 +0000 Subject: [PATCH 09/10] Apply 1 suggestion(s) to 1 file(s) --- docs/editor.md | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/editor.md b/docs/editor.md index 2077755d3..8c8b1fc9b 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -153,6 +153,7 @@ initialisation file: (":>" . ":=") ("by" . "now") ("forall" . "now") ;; NB: this breaks current ∀ indentation. + ) ``` This will let the indentation strategy treat the Iris symbols (e.g. `-∗`) similar to the closely related Coq symbols (e.g. `->`). -- GitLab From f486ef4e0028db8bb3b42fdd9838a06021c42c9c Mon Sep 17 00:00:00 2001 From: Jonas Kastberg Hinrichsen Date: Wed, 11 May 2022 16:24:33 +0200 Subject: [PATCH 10/10] Added one more missing parenthesis --- docs/editor.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/editor.md b/docs/editor.md index 8c8b1fc9b..0933ff190 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -153,7 +153,7 @@ initialisation file: (":>" . ":=") ("by" . "now") ("forall" . "now") ;; NB: this breaks current ∀ indentation. - ) + )) ``` This will let the indentation strategy treat the Iris symbols (e.g. `-∗`) similar to the closely related Coq symbols (e.g. `->`). -- GitLab