Zulip Chat Archive

Stream: general

Topic: Porting declaration


Yaël Dillies (May 30 2021 at 18:59):

I'm writing a (short) module docstring for order/zorn and I noticed the "porting declaration" Ported from Isabelle/HOL (written by Jacques D. Fleuriot, Tobias Nipkow, Christian Sternagel). was in the copyright header. Is that accepted practice? I would instead do something like

/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl
-/
import ...

/-!
...

## Notes

Ported from Isabelle/HOL (written by Jacques D. Fleuriot, Tobias Nipkow, Christian Sternagel).
-/

Should we (/have we) write down our standard for porting declarations somewhere in the non-maths docs?

Bryan Gin-ge Chen (May 30 2021 at 19:14):

Your suggested format looks good to me, and yes, it would be good to document that sort of thing here: https://leanprover-community.github.io/contribute/doc.html


Last updated: Dec 20 2023 at 11:08 UTC