Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • T thesis-projects
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 47
    • Issues 47
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • KWARC
  • thesis-projects
  • Issues
  • #21

Closed
Open
Created Jul 25, 2018 by Michael Kohlhase@mkohlhaseOwner

Data Dimension for MathHub.info

The MathHub.info system currently only has active/semantic documents and theory graphs. But we would like to integrate and host mathematical data bases like the OEIS or LMFDB with mathematical interfaces.

The theory and part of the implementation has already been done in virtual theories and is proposed as part of #20. Now we need to build the infrastruture in MathHub.info. Concretely, this involves

  • installing and exposing a data base server as http://data.mathhub.info (probably Postgres or so)
  • extending the MMT lmh extension to create data bases for any archive with virtual theories (i.e. theories for which the necessary codecs and schema theories exist)
  • developing a process for syncing the access permissions in the data base with those for the archive at http://gl.mathhub.info
  • develop a MMT data extension with a structure component that creates/updates tables for MMT theories and whose object component uses queries for MMT expressions.
Assignee
Assign to
Time tracking