Porting declaration

Stream: general

[Yaël Dillies]

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]

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