Skip to content

Chaining module <+ operator shows quadratic time increase #22279

Description

@ebmoon

Description of the problem

Image

When chaining modules by <+ operator, the time to build module increases quadratically to the number of chained modules.

Script for plot: modulechain.py

Small Rocq / Coq file to reproduce the bug

Version of Rocq / Coq where this bug occurs

Checked in version 9.2

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response

Metadata

Metadata

Assignees

No one assigned

    Labels

    kind: performanceImprovements to performance and efficiency.part: modulesThe module system of Coq.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions