coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Safe to download and compile .v from evil source ?

From: Andres Erbsen <andreser AT mit.edu>
To: coq-club AT inria.fr, Jay Kruer <kruerj AT reed.edu>
Subject: Re: [Coq-Club] Safe to download and compile .v from evil source ?
Date: Sat, 01 Feb 2020 17:41:27 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=andreser AT mit.edu; spf=Pass smtp.mailfrom=andreser AT mit.edu; spf=None smtp.helo=postmaster AT outgoing.mit.edu
Ironport-phdr: 9a23:BT6S5x2tV5yl4rrusmDT+DRfVm0co7zxezQtwd8Zse0fIvad9pjvdHbS+e9qxAeQG9mCt7QY0aGP7fuoGTRZp8rY6zZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJ6KevvB4Hdkdm82fys9J3PeQVIgye2ba9vIBmsogjdq8YbjZFtJ6ovxRfFv3pFdupLzm9sOV6fggzw68it8JNt6Shcp+4t+8tdWqjmYqo0SqBVAi47OG4v/s3rshfDTQqL5nQCV2gdjwRFDQvY4hzkR5n9qiT1uPZz1ymcJs32UKs7WS++4KdxSR/nkzkIOjgk+2zKkMNwjaZboBW8pxxjxoPffY+YOOZicq7bYNgXXnRKUNpPWCNdA4O8d4oPAPQHPeZEtIn2ul8CoQKjCQWwGO/jzzlFjWL006InyeQsCQ/I0w4uH90BrHvao8j7OrkSX+6216TH1zfOb/ZM1Dvh9ITFcBYsquyMU7JqdsrRzFEiGh/DjlqNs4zqISiV3fkCvWiB9OVgTvygi2g6oAx2uDevwNojipPXiYIO1F/E7z50wIM0Jd2kUkJ0f8OrEIZJuiycKoB4QdsiTnl1tCs50LELvYS3cDYJxZg92hLTduSLf5WM7x79TuqcJTN1iGhqdb6hnRq+7EytxvH6W8KpylhFtDBFncPJtn0V1xzc9MyHSvxl80emxDaPyw/T6uZFIUAymqrXMZshwr8slpYJr0vMAzL2lF33jK+QaEok5vCl5/nkb7n8opKQLZF4hwLkPqgzh8CzGeE4PRIPX2if9+S8zrrj/UjhTbpQiP05j7PZv47BJcsFvK60GApV0oc/6xqlETipzckYkWEdLF1ZYBKHk5TpO1bWLf/kCve/mk2gnytvx/DbJbLsGY7NL3jGkLf5Z7lx8U9cyAwpzdBe/Z1YEL8BIOigEnP24dffF1oyNxG+6+fhEtR0kI0EHSqtC77RE7nPvEXAsuE1PuSWZqcPtTvxbfUp+qi9o2U+nAo0e6Wz0IBfRWqyBflgaxGQZ3b2j8wMC08PvxZ4QeD33g7RGQVPbmq/CvpvrgowD5irWMKaHtj00e6xmRyjF5gTXVhoT1WFEHPmbYKBCqUJaT7UL8N8wGVdCeqRDrQ53BTrjzfUjqJ9J7uG/ywE85/vyYotvrCBpVQJ7TVxSv+l/SSNQmVzxzNaQCIq06d+p0M7z1afl6V0nq4AGA==

Redirect and Extraction commands write to the disk by spec. I reported it a while back and was told that I shouldn't expect coqc on unknown code to be safe in any sense.

[Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/01/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Jay Kruer, 02/01/2020
  - Re: [Coq-Club] Safe to download and compile .v from evil source ?, Andres Erbsen, 02/01/2020
    - Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/01/2020
    - Re: [Coq-Club] Safe to download and compile .v from evil source ?, Tej Chajed, 02/01/2020
      - Re: [Coq-Club] Safe to download and compile .v from evil source ?, jonikelee AT gmail.com, 02/02/2020
      - Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
      - Re: [Coq-Club] Safe to download and compile .v from evil source ?, Clément Pit-Claudel, 02/02/2020
        
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
        
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, jonikelee AT gmail.com, 02/02/2020
        
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Marco Servetto, 02/02/2020
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Jason Gross, 02/02/2020