coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Erik Martin-Dorel <e.mdorel AT gmail.com>
- To: coq-club AT inria.fr
- Cc: proof-general-maintainers AT groupes.renater.fr
- Subject: Re: [Coq-Club] newlines misparsed as space in emacs+proof-general+company-coq
- Date: Fri, 14 Jun 2024 21:24:47 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e.mdorel AT gmail.com; spf=Pass smtp.mailfrom=e.mdorel AT gmail.com; spf=None smtp.helo=postmaster AT mail-ej1-f50.google.com
- Ironport-data: A9a23:KgoUB6Ne0E86iOzvrR2YnMFynXyQoLVcMsEvi/4bfWQNrUoi0DxUz 2cZWWGCa/feMzOmeN4ja4S+8kkC7ZfSyoAwSHM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/vgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5OZYA/NNwJcaDpOt/rd8U835pwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGXhIknuw+szL3sKLIMGw9ZtBV8X9 P4XfWVlghCr34pawZq+Q+how8khdYzlYdtZtXZnwjXUS/0hRPgvQY2QvY4ejGp23JkeW6uGD yYaQWIHgBDobltKNlANBZYWk+Khh325eDpdwL6QjfNouzeNkVcogNABNvLQZIyFGcdZn32lu 0PH4XvoMw8EOOOAnG/tHnWEw7ancTnAcIkVDfiz8uNgqEaCw3QaThwQT1qy5/ej4nNSQPpaI k0Qvycs9O08qRTtQd76UBm15nWDu3bwRua8DcUduTOPyrSJwDylF2Yadw5bbOJ/tc05EGlCO kCyo/vlAjlmsbuwQH2b96uJoT7aBRX5wEcHbC4ACAYHupzt/dl1gRXIQdJuVqWyi7UZ+A0cI Rjb9UDSYon/a+ZVis1XGniZ31qRm3QwZlddCv/rY45R1SsgPNTNT9XwtzDztK8cRK7HFAXpl CZfwKC2srteZaxhYQTXH43h6pnyt6jbWNAd6HYzd6QcG8OFpyf9J94NuGshfy+E8K8sIFfUX aMagisJjLc7AZdgRfYfj1uZUp9xkfrTBp7+W+rKb9FDRJF0eUXVtGttfEOclSSl2kQljah1a 9/RfNeOHEQqL/1t7AO3YOMBjp4t5CQ1nl3ISb7Bkh+I7Lu5ZVyuc4kjDmegVO4D0f67kF3ny OoHb8qu4DdDYdL6eRjSoNIyL0hVDH0VBqLWis1wd8yFKDVIAGsKVv3bm+sgX6dHnK1lsPjC0 V/ge01fyXv53WbmLyfTYF9dSbrfZ7RNhlNlAj4NZHGDxGoGTbu0ypsmZ78bXOUC5fM56+xZV NwHStWkLtUUbQqf4BUbT532jLI6RSSRnQjUYhaUOmkuTaBvVyni24HBbADw0AIsEyDul881g 4P45zPhWZBZGjhTVpfHWsmOkWG0k2MWwt9pfk3yJdJWRkXg3a5qJwH1jd41O8s8EgrC9BTLy zepBQokmseVr78X6NXpgYW2n7WtGcZ6HWtYGDD/xpSyPi/44GGi4NFhVMClQDPjb173qZ6SP bht8/LBMfM8jAlrtah4GO1V1q4Q3YbkiIJb6QVGJ0/1SWqXJIluGVS4+PVel7Zsw+ZZsDSmW 0jU9dh9P66ICfzfE1UQBVQEa72D3M4Lhgvt6uQRH3SjwQQq+rDdAENYECSRuXYMMJp0L4IX7 uMzs+EG6wGEq0QLM/TXqgt25mizPng7fKF/ja4jAajvkRgO5mBZR57XGgvawcioRY1XE08IJ jS0uvLzt45EzBCfT0tpRGn/4+VNoL8v5jZI9QYmDHaUkIPngvQX4kVgwQ4vRF4I8iQdgvNBA Uk1BUhbPq7UwixJgvJEVGWSGw1sIh2V10jy6lkRnl3iUEiaeT3RHVI5JNqy0hgVw0BEchhf2 YOo+mLvfDLpXcP2hw8Ze0purd79Rt1QqCzGvu2aHPq+IpprWgq935eSZlcJpSD3XuI3pknM/ tdx8MhKNKbUCC83oo8AMbe864g+ch6/CVZ5calTx59RRWD4UxOu6AeKMHG0K59sJeSV0EqWC P5OB8NoVja43hmgtjowWKwGeed1uNUL59MyXKzhCkBbkrmYrxtv6Inx8AqnjkAVYtxeq+QPA aKPSCCjS0u7mmlxt1LWivV9Kk6UQIUhdRKm+vKY68ALJoInnMA3Vn9qyZqynXGeEDU/ziKup AmZOpPnlb1z+7pjj67HM/tmFQ6rDfjRSe7R0gS4k+oWXOP1Kc2U6j8k8Aj2DT93Y4kUdc98z 4mWkdjN20jAgrY6fkbZl7SFFIhL/c+CZ/VWAO2mMEhlmTa+Z+G07ysh42yYLbl7oOFZ7OSjR Cq6b5KUXvwRUNF/2nZUSnZ/FzAwNqfJVZrj9BiN96m0Nhsg0AL8PIyG813tZjplbSMmAcD1J TL1nPeM3epmirpwKiUKPNxcOK8hAnHedLsUSfChtB2zLHWZvVeZi76zyTsi8W7qD1eHIubb4 LXEZBz0cjGusoHM0ttY7pJ5uxYWKF1fguAAWF0X1PArqjK9DU8Adf88N7dfAL5qsyXC7rPKT xCTU3kDUALTBS9ldzf46/TdBjavPPQEYIrFF2Z47nGqZDeTL6LeJrlYrwNLwWp8Ixnnx8GZc eAuwGX6ZEWN88s4VNQox6KJhMl8zann3VMOw0f2lvLyDzs4Abkn0H9AHhJHZRfYEvPixVn6G mwoeV9qGE2La1b9McJFSU5nHBs0uDDOzTJxSQytxN3ZmZuQzcwe6fnZFtzw7IY+b5UxFOZTf U/0emqD3TnHkDhb864koMkgjqJIGOqGVJryZrPqQQoJ2bq88CI7NscFhjACV9wm5BUZKV7Gi z2w+DIrMSxp8qyKNGG+km3lOq6dU07gyxnMhQ/74DLEyFk3koCfdB+twwb2b5r3rsAPeqmer Cg6NC6sT5++7VMIZgWSctwUo1WGBYcaEnysvuUAUMbpihn1IINCPOkJ7qz5vu69NFVLw4xVc OCa1NBVFEdLmM+Q91iMoer1qYSLY1vM9srvRlMpEN9W+gOM6b7G
- Ironport-hdrordr: A9a23:tvl21aGuKr5M4UvKpLqE3ceALOsnbusQ8zAXPo5KOGRom62j5r uTdZEgvyMc5wxhPE3I9erwXZVoBEmslqKdgrNxAV7BZniAhILAFugLhrcKgQeBJ8SZzJ8+6U 4KSdkZNDSfNykCsS842mWF+hQbreVvPJrGuQ4W9RlQcT0=
- Ironport-phdr: A9a23:QJL9BxCWytmE3i4fzBQRUyQUFkoY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua88ygSQDM6CsK4MotGVmp6jcFRD26rJiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wE ZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmj6wbal8I RmrqQjdudQajIVtJ60s1hbHv3xEdvhZym9vOV+dhRHw6Nuu8pV+6SpQofUh98BBUaX+Yas1S KFTASolPW4o+sDlrAHPQgST6HQSVGUWiQdIDBPe7B7mRJfxszD1ufR71SKHIMD5V7E0WTCl7 6d2VB/ljToMOjAl/G3LjMF7kaVUrg+8pxxk247bfp2aNOZwcKPaeNMVX2tBXsBMXCBFDY6xa 44DAuwcNuhasob9vUMDohSwBQauHuPhyjFGiHzr06MkzekuDRrL0xY8E98UqnnYsMn5OaUUX OuozKfI1zLDb/ZO1Dny8ojIcxMhquyLU71qa8rR1UgvFwXcgluerozlJS2a1uAQuGWc8eVsT +evhHMgqwFrvDevwtwhiobMho0Py1DE8T91z5oyJd29UUN2Z8OvH5RMuS+ALYR2Xt8iTH9yu CY80rAKpZ+2cSkFxZg6yBPSaeGLfYiK7xzjV+ucPyl1iXFrdr+9hxi/9VSsxvP+W8e701tHq jRJn9bDu30MyRDf99WLR/1g9Umv3jaP0hrc6uBCIU0smqrbKoIhwr4tlpUIq0jMAij2mEDug K+IaEok4PSn5PrjYrn8vJCcL5d0hhniPaQpgMy/B/o3MgwKX2SB5+uzyaDj8VX8QLpQlP02j qjZsJbDKcsGoa65GRFa0oI55xa4FTem39IVlmQEIlJdYB+LkZTlNlXULP37DfqzmUqgnCpoy vzcPrDtHpPAJWXdnbflYLZ98FJcxxQpzd5C5pJVC68OLervVkL3qdfWFAU2MxauzObiENh91 p0RWWaIAqKBNaPdq16I5uY2L+aSZo8ZpS/xK/Yl6vLyl3M5llgdfa6m3ZsTdn+0BOhpI0KcY Xb0g9cBF3kFvhYmQeD0lFGPVSRfanWyUq4m+D03FYGrAZ3DS4yxmLCB2T20HpxSZmBIEFCMF nLoep2aVPsWbSKdP8hhkiYaWrilUIIh2hSuuxX7y7pjNObb5ioYtZf72Nhz/OLcjQsy+iBsD 8SBz2GNSHl5kn4QSz8swK9/uVB9ykuE0aVgn/NYEsVT6+pVXQc+KJ7T1Pd3C8vyWwLEZteGU kyqQtSgATErT9I+2cUCY0hnG4bqsheW1C2zRrQRirajBZou86ua0WKiHctlz2f60/wslVglB M5GL3GngOtz8BLeA6bElV7ck7etc+IbxiGe2n2EyD+jpkBbGCt5S7nEWzUzYVHbqZyt6wXHQ 7i0BLAPPQ5IyMrEIaxPPI66xW5aTevubYyNK1m6nH29UErZrlvtRI/jemFHmT7YFFBBiQcYu 3CPKQk5AC6l5WPYFj1nU1z1MAv36ecrjnS9Qwcvyh2SKVV73u+4vBsZguaRT9sc27sFvGEqr DAnVE2l0YfuAsGb7xFkYL0aZNo85Fld0meMukp4Mpu6IqRKiVsXcgAxtETrhF1sEosVt88so TsxyRZqb6KV1FQUbzSDwZX5IaHaMEH39RGrLqPUgxTQjY7Q9aAI5/A17V7kuWlFD2IE9HNqm 5lQ2nqYvNDRCRYKFIj2WQAx/gR7oLfTZm884ZnV3DtiK/v8tDiKwN8vCOY/r3ToN95CLKOJE hPzGMwGFoCvLuItgV2gchMDOqhb6qc1O8qsc/bO1rSsOa5smzevjGIP544YsArE+mx5RunS0 pItzPSR3w/BXDD5zR+gvs3xhYFYdGQKBGPsgSPgBYNXeuhzZdNRUTboc5DxnIwuwcO1CBs6v Ba5ClgL2dGkY0+XZl35h0hL0FgP5Gagkm2+xiB1lDcgquye2jbPyqLsbkliWCYDSW98gFPrO YXxgcodWR3iYk4smBy/6ELSyK1SpaA5JG7WCxQtHWC+PyR5X628u6DXKcMJ7Z8vqyhTeOu5a FGeDLX6plFJmzOmFGxYyjchcjissZishB12hlWWK3NrpWbYc8V9rfvGzOTVXuUZnj8PRS0iz CLSGkD5Jd6iu9Odi5bEtOm6EWOnTJxaNyfxn8uMsy6y5GsiBhPa/bj7l5viHQ8g3CvT2NxjV CGOpxH5KoXmzKW1N+t7c1IgXgetrZonXNsnws1t3NkZwjACi4+Q/GYbnGuWU50Twq/4YHcXB HYKz9PT/An5yRhmJ3ONyZj+UybVyc9gat+mJ2IOj3hlvoYaVeHOtewCwHMmxzjw5RjcavV8g DoHnP4n6XpAxvoMpBJo1CKWRLYbAUhfOyXo0RWO9dG36qtNNwPNOfC90lRzmde5AfSMuAZZD Tz0PJIuGjV96u1wNVvN1Dv47YSuK7yyJZoD8waZlRvNlb0fJdQ0mv0QiC5PNmf0vHljwOk+x 08mzdSxu46JLH9o9aSyD0tDNzH7UMgU/ynkkadUmsvFuuLnVoUkADgAW4HkCO65CD9H/+qyL B6ASXdv4mfeA7fUGhWTrVtrv26aWY7+LGmZfRx7hZ1jXEXPfxEZ2VFMGm9mwdhhUVr2jM35L BUnunZLvQW+80UUjLovbki3U3+D9ln2LG5sEt7HakIRtFknhQ+dMNTCvLwtWXsEr9vx9ErVb TbDLwVQUTNWAArdWxa6b+PovZ6Zo6CZHrbscKeIOO/T77QYD7DRm/fNmsNn52reb53feCA9U LtrnBIEBykxGtyFyWxQEGpOxn6LN4jD407isixv8pLlqKWtCF+pvNHfTeMVaIoKmVj+gL/fZ bTJ2mAkeXABh8lKnTiRmfAexAJA0XgwMWP2QPJb72iVC/uB0rleCxpRA89qHO1P6a90ngxEO MqBz8jwyqY9lPk+TVFMSV3mnMitI80MOWC0cl3dVg6NM/ydKDvHztuSA+v0QKBMjOhSqxy7u CqKW07lMDOZkjD1VhepeehShSCfNRZatcmzaBFoQWTkSdvnbFW8ProVxXUuxqYog3rRKWMGG T11ckcIo7/JqC0F2rNwHGtO6ncjJu6B2m6Y4+TeNpcKoK5rDyBzxIc4qDwxz7pY6j0BReQgw nOD6I4z5Qv/wq/SkmkCMlIGsDtAiYOVsF83PKzY8sMFQnPY5FcX6m7WDR0WptxjA9mpuqZKy 9GJmrigTVUKu9/S48YYANDZbcydN390exevHTLTFgYBZTGuPGDbwUdalbvBkx/d5oh/sZXql JcUH/VDU0cpE/oBFkl/NNkLIZMyUzF91LDG1IgH4n2xqBSXT8Jf9MOiNLraEbDkLzCXiqNBb h0DzObjLIgdAYb83lRrdlhwmImi86/4UtVEoyknZQgx8h0lGJlWS2Qy3wfoaFro7iJLU/Gzm REyh011ZuF/rF8EDH84I1PLoG07l0xjwL3Y
- Ironport-sdr: 666c990c_k3tIOqvcPuzHmEBSewt6IOkYuaSs/zCdbIdi/oMdJtjk0uo K9F7i3YB0PdFqdaSgEmrvyR+5+jATX5UNmGd+YA==
Thanks Abshishek,
Yes, this looks like a side-effect of PG's pre-processing phase.
I opened an issue in https://github.com/ProofGeneral/PG/issues/773
Best regards,
Erik
Le ven. 14 juin 2024 à 20:19, Abhishek Anand <abhishek.anand.iitg AT gmail.com> a écrit :
When I enter the following in a new file, I get:
Require Import Coq.Strings.String.
Definition foo: string :=
" a
".
Set Printing All.
Compute foo.
(*
= String (Ascii.Ascii false false false false false true false false)
(String (Ascii.Ascii true false false false false true true false)
(String (Ascii.Ascii false false false false false true false false) EmptyString))
: string
*)
The last character of foo is a newline but it is parsed as a space (ascii 32 (0x20)).
However, when I compile it using coqc, or interactive run it in jscoq (https://coq.vercel.app/), I get the correct answer:
=String
(Ascii.Ascii false false false false false true false false)
(String)
(Ascii.Ascii true false false false false true true false)
(String)
(Ascii.Ascii false true false true false false false)
false
EmptyString
: string-- Abhishekhttp://www.cs.cornell.edu/~aa755/
--
- [Coq-Club] newlines misparsed as space in emacs+proof-general+company-coq, Abhishek Anand, 06/14/2024
- Re: [Coq-Club] newlines misparsed as space in emacs+proof-general+company-coq, Erik Martin-Dorel, 06/14/2024
Archive powered by MHonArc 2.6.19+.